|
|||||
|
|
| 实例化空间:一种新的安全协议验证逻辑的语义模型 | |
| 引用本文： | 苏开乐,岳伟亚,陈清亮,ZHENG Xi-Zhong. 实例化空间:一种新的安全协议验证逻辑的语义模型[J]. 计算机学报, 2006, 29(9): 1657-1665 |
| 作者姓名： | 苏开乐 岳伟亚 陈清亮 ZHENG Xi-Zhong |
| 作者单位： | 1. 中山大学计算机科学系,广州,510275 2. 中山大学计算机科学系,广州,510275;勃兰登堡州理工大学计算机科学系,科特布斯,03046,德国 3. 勃兰登堡州理工大学计算机科学系,科特布斯,03046 德国;江苏大学计算机系,镇江,212013 |
| 基金项目： | 国家重点基础研究发展计划(973计划);国家自然科学基金;广东省自然科学基金;教育部留学回国人员科研启动基金;教育部<新世纪优秀人才支持计划>资助项目;德国研究项目;中山大学校科研和教改项目;上海市重点实验室基金 |
| 摘 要： | 给出了一个称为“实例化空间（instantiation space）”的安全协议验证逻辑的语义模型．该语义模型是建立在一种自然的加密信息交换（cryptographical message exchange）模型上的．在此语义模型基础上，文章提出了一系列与安全属性相关的验证公理，由此可以证明它们在此语义模型下的正确性．更重要的是，在此语义下的公理集在算法上是完全可以实现的，其对应的工具SPV（Security Protocol Verifier）已经开发成功，并且可以验证复杂的协议．在这套安全协议验证模型理论下，可以很方便地处理包括公钥、私钥、共享密钥和Hash函数组成的复杂信息格式．而且，在此语义基础上的公理集是纯命题逻辑的，因此所需要的验证目标可以很方便地转化成可满足性问题（SAT），从而可以利用工业上快速高效的SAT求解器实现． |
| 关 键 词： | 实例化空间 加密信息交换模型 可满足性问题 |
| 收稿时间： | 2006-04-01 |
| 修稿时间： | 2006-04-012006-05-30 |
Instantiation Space: A New Model for Security Protocol Logic |
|
| SU Kai-Le,YUE Wei-Ya,CHEN Qing-Liang,ZHENG Xi-Zhong. Instantiation Space: A New Model for Security Protocol Logic[J]. Chinese Journal of Computers, 2006, 29(9): 1657-1665 | |
| Authors: | SU Kai-Le YUE Wei-Ya CHEN Qing-Liang ZHENG Xi-Zhong |
| Affiliation: | 1. Department of Computer Science, Sun Yat-Sen University, Guangzhou 510275; 2. Department of Computer Science, Brandenburg University of Technology, 03046 Cottbus, Germany; 3. Department of Computer Science, Jiangsu University, Zhenjiang 212013 |
| Abstract: | |
| Keywords: | |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |