密码协议的秘密性证明  

Proving Secrecy Property of Cryptographic Protocols

作　　者：胡成军[1,2] 郑援[3] 沈昌祥[4] 

机构地区：[1]中国科学院研究生院信息安全国家重点实验室 [2]海军潜艇学院青岛266071 [3]海军潜艇学院 [4]海军计算技术研究所

出　　处：《计算机学报》2003年第3期367-372,共6页Chinese Journal of Computers

基　　金：国家"九七三"重点基础研究发展规划项目"信息与网络安全体系结构研究"(G19990 3 5 80 1)

摘　　要：在Paulson的归纳方法基础上提出一种新的密码协议秘密性的证明方法 .该方法在消息事件结构中引入会话标识符 ,给出协议满足秘密性的充要条件 ,大大简化了协议秘密性的证明 。In this paper, a new method based on Paulson's inductive approach for proving cryptographic protocols' secrecy property is proposed. The message and event structure are extended with a special session identifier. A sufficient and necessary condition for a protocol to satisfy its secrecy specification is given. With this condition, protocol's secrecy proof is greatly simplified. Experiments show that this approach is efficient and suitable for mechanical implementation.

关 键 词：密码协议 秘密性证明 密码学 随机数 定理证明 信息安全 

分 类 号：TN918.1[电子电信—通信与信息系统] TP309[电子电信—信息与通信工程]