串空间模型的原理与应用  

Theory and application of strand spaces model

作　　者：谭立力[1] 刘璟[2] 谢鸿波[3] 谭兴烈[1] 

机构地区：[1]卫士通信息产业股份有限公司 [2]现代通信国家重点实验室,四川成都610041 [3]电子科技大学计算机科学与工程学院,四川成都610054

出　　处：《计算机应用》2005年第8期1747-1749,1752,共4页journal of Computer Applications

基　　金：现代通信国家重点实验室基金资助项目(51436040305DZ4001);国家重点基础研究发展规划资助项目(G1999035803)

摘　　要：介绍了安全协议形式化分析方法串空间模型的基本概念,给出了检查消息机密性的定理的变形公式,形式化地证明了由未泄漏私钥签字的消息起源于诚实主体串,并利用上述结论检验了BAN修改后的CCITTX.509(3)协议的机密性和认证性。The basic notion of strand spaces model was introduced, then a equivalence formula checking secrecy of messages was given, and it was proven that a signed message by a confidential private key had its origin in a honest strand. Finally these two conclusions were used to check BAN modified version of CCITT X.509(3) protocol.

关 键 词：密码协议 串空间 CCITT X.509协议 

分 类 号：TP309.2[自动化与计算机技术—计算机系统结构]