《计算机学报》文章摘要   全文下载
文章题目	实例化空间：一种新的安全协议验证逻辑的语义模型
作者	苏开乐1) 岳伟亚1) 陈清亮1)，2) ZHENG Xi-Zhong2),3)
作者单位	1)(中山大学计算机科学系 广州 510275) 2)(勃兰登堡州理工大学计算机科学系 科特布斯 03046 德国) 3)(江苏大学计算机系 镇江 212013)
发表年份	2006
发表月份	9期(1655—1663)
文章摘要	摘要 给出了一个称为“实例化空间(instantiation space)”的安全协议验证逻辑的语义模型.该语义模型是建立在一种自然的加密信息交换(cryptographical message exchange)模型上的.在此语义模型基础上,文章提出了一系列与安全属性相关的验证公理,由此可以证明它们在此语义模型下的正确性.更重要的是,在此语义下的公理集在算法上是完全可以实现的,其对应的工具SPV(Security Protocol Verifier)已经开发成功,并且可以验证复杂的协议.在这套安全协议验证模型理论下, 可以很方便地处理包括公钥、私钥、共享密钥和Hash函数组成的复杂信息格式.而且,在此语义基础上的公理集是纯命题逻辑的,因此所需要的验证目标可以很方便地转化成可满足性问题(SAT),从而可以利用工业上快速高效的SAT求解器实现. 关键词 实例化空间; 加密信息交换模型;可满足性问题 中图法分类号 TP309