NS公钥协议新的分析方法

A New Analysis Method of NS Public-key Proctocol

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

It is an important and hard problem in the area of computer network security to analyze cryptographic protocols.A methodology of NS public-key proctocol is presented based on functional programming language Haskell.When formaling the model,Dolev-Yao intruder model is assumed,and based on state transition system,message and events are semantically encoded,security properties are described by event sets.It proposes inspection strategy for security properties.The features of lazy evaluation of Haskell have solved some key problems which are formal specifications for security protocols with this analysis method,which successfully find the Man-in-the-Middle Attack.