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

摘要：

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

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

所属期刊栏目：37

分类号：TN915.04

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

在线出版日期：2015-11-10（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：1850-1855