基于事件逻辑的改进NeedhamSchroeder协议安全性证明

来源：计算机工程与科学杂志2015年第10期北京时间：

作者：刘欣倩，肖美华，程道雷，梅映天，李伟

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

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

关键词：事件逻辑,改进的Needham-Schroeder协议,形式化方法,强认证性理论,

基金资助：国家自然科学基金资助项目(61163005)；计算机软件新技术国家重点实验室开放课题资助项目(KFKT2012B18)；江西省自然科学基金资助项目(20132BAB201033)；江西省高校科技落地计划资助项目(KJLD13038)；江西省对外科技合作技术资助项目(20151BDH80005)；华东交通大学研究生创新计划资助项目(YC2014X007)