NS公钥协议新的分析方法

摘要：

密码协议安全性的分析是当前网络安全研究领域的一个世界性难题.在函数式程序设计语言haskell中给出一种NS公钥协议的分析方法.在形式化建模时,以Dolev-Yao攻击者模型为前提假设,状态转移系统为框架,用语义编码的方式定义消息和事件,用事件的集夸来描述协议的安全属性,并给出安全属性的检验策略.Haskell的惰性计算特性解决了对协议形式化分析的语义描述等关键问题,发现了NS协议的中间人攻击.

关键词：网络安全、安全协议、形式化分析、模型检测方法NS公钥协议

所属期刊栏目：6

分类号：TP393(计算技术、计算机技术)

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

页数：共3页

页码：3011-3013