【摘要】 在Paulson的归纳方法基础上提出一种新的密码协议秘密性的证明方法 .该方法在消息事件结构中引入会话标识符 ,给出协议满足秘密性的充要条件 ,大大简化了协议秘密性的证明 ,高效且适合机械化实现更多还原

【Abstract】 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.更多还原