NS公钥协议新的分析方法

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