实例化空间:一种新的安全协议验证逻辑的语义模型

摘要：

给出了一个称为"实例化空间(instantiation space)"的安全协议验证逻辑的语义模型.该语义模型是建立在一种自然的加密信息交换(cryptographical message exchange)模型上的.在此语义模型基础上,文章提出了一系列与安全属性相关的验证公理,由此可以证明它们在此语义模型下的正确性.更重要的是,在此语义下的公理集在算法上是完全可以实现的,其对应的工具SPV(Security Protocol Verifier)已经开发成功,并且可以验证复杂的协议.在这套安全协议验证模型理论下,可以很方便地处理包括公钥、私钥、共享密钥和Hash函数组成的复杂信息格式.而且,在此语义基础上的公理集是纯命题逻辑的,因此所需要的验证目标可以很方便地转化成可满足性问题(SAT),从而可以利用工业上快速高效的SAT求解器实现.

关键词：实例化空间、加密信息交换模型、可满足性问题

所属期刊栏目：29

分类号：TN91

资助基金：国家重点基础研究发展计划973计划2005CB321902;国家自然科学基金60496327;10410638;60473004;广东省自然科学基金04205407;教育部留学回国人员科研启动基金;教育部<新世纪优秀人才支持计划>资助项目;德国研究项目DFG446 CHV113/240/0-1;中山大学校科研和教改项目;上海市重点实验室基金

在线出版日期：2006-11-07（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：1657-1665