共 3 条
公平交换协议的一个形式化模型
被引：10
作者：
卿斯汉
李改成
机构：
[1] 中国科学院软件研究所信息安全技术工程研究中心
[2] 北京中科安胜信息技术有限公司
[3] 中国科学院研究生院 北京
[4] 北京
来源：
基金：
北京市自然科学基金;
关键词：
事件;
局部因果关系;
局部时序关系;
全局关系;
交换项;
安全目标;
D O I：
暂无
中图分类号：
TP393.09 [];
学科分类号：
080402 ;
摘要：
基于对现有公平交换协议的研究, 使用求精过程建立了精确的形式化结构模型, 在这一过程中, 使用不可靠信道模拟攻击行为. 模型首次给出了交换项的形式化定义, 提出的公平性、可追究性目标能够更加完整地反映公平交换协议的内在要求. 为了能高效而又细致地对协议进行检测、证明和设计, 模型提出了适用于所有公平交换协议的不可滥用性的新性质, 给出了第三方可信赖串的定义和设计安全高效的公平交换协议的一般准则. 文中通过一个典型的公平交换协议分析实例, 阐明了使用该模型分析公平交换协议的详细步骤. 发现了一种过去从未发现过的新攻击, 给出了攻击发生时系统运行的全过程, 深刻揭示了攻击发生的各种原因. 最后, 对有缺陷的协议进行了改进, 改进后的协议满足所需要的各种性质.
引用
收藏
页码：161 / 172
页数：12
相关论文