摘要：安全协议是现代网络安全的基础,密码协议的安全性证明是一个挑战性的问题.事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于刻画安全协议的形式化描述,是定理证明的基础.用事件序语言、事件类和一个表示随机数、密钥、签名和密文的原子类,给出身份认证协议可以被形式化定义和强认证性证明理论.利用该理论对增加时间戳的Needham-Schroeder协议安全性进行证明,证明改进的Needham-Schroeder协议是安全的.此理论适用于类似复杂协议形式化分析与验证.

关键词：事件逻辑 形式化方法 强认证性理论 

单位：华东交通大学软件学院 江西南昌330013