公平交换协议的一个形式化模型  

作　　者：卿斯汉[1,2,3] 李改成[1,2,3] 

机构地区：[1]中国科学院软件研究所信息安全技术工程研究中心 [2]北京中科安胜信息技术有限公司,北京100080 [3]中国科学院研究生院,北京100039

出　　处：《中国科学（E辑）》2005年第2期161-172,共12页Science in China(Series E)

基　　金：北京市自然科学基金(批准号: 4052016);国家自然科学基金(批准号: 60083007);国家重点基础研究发展规划(973)(批准号: G1999035802)资助项目

摘　　要：基于对现有公平交换协议的研究, 使用求精过程建立了精确的形式化结构模型, 在这一过程中, 使用不可靠信道模拟攻击行为. 模型首次给出了交换项的形式化定义, 提出的公平性、可追究性目标能够更加完整地反映公平交换协议的内在要求. 为了能高效而又细致地对协议进行检测、证明和设计, 模型提出了适用于所有公平交换协议的不可滥用性的新性质, 给出了第三方可信赖串的定义和设计安全高效的公平交换协议的一般准则. 文中通过一个典型的公平交换协议分析实例, 阐明了使用该模型分析公平交换协议的详细步骤. 发现了一种过去从未发现过的新攻击, 给出了攻击发生时系统运行的全过程, 深刻揭示了攻击发生的各种原因. 最后, 对有缺陷的协议进行了改进, 改进后的协议满足所需要的各种性质.

关 键 词：公平交换协议 形式化模型 局部时序关系 安全目标 电子商务 安全技术 网络安全 

分 类 号：TP393.09[自动化与计算机技术—计算机应用技术]