安全协议的测试与证明

Testing and proving security protocols

提出通过测试来证明安全协议的方法。以NS和NSL协议为例,首先将协议形式化为事件序列,协议的性质可以表示为序列上的性质。协议的完整运行可以系统地生成,因此,协议的性质可以系统地测试。形式化和测试在函数程序设计语言Haskell中完成。

It is shown how security protocols can be systematically tested,hence proved in Haskell.That is demonstrated by analyzing NS（Needham-Schroeder） and NSL（Needham-Schroeder-Lowe） protocols：runs of the protocols are formalized as event traces and properties on traces are tested.Complete runs of a protocol with a penetrator can be generated systematically,and properties of the protocol can be tested systematically.Lowe＇s attack is easily revealed by testing NS protocol and authentication and secrecy are proved valid for NSL protocol by testing.