Computer Engineering and Applications ›› 2009, Vol. 45 ›› Issue (4): 26-29.DOI: 10.3778/j.issn.1002-8331.2009.04.008

• 博士论坛 • Previous Articles     Next Articles

Testing and proving security protocols

QIAO Hai-yan   

  1. Zhongshan University,Guangzhou 510275,China
  • Received:2008-09-19 Revised:2008-11-10 Online:2009-02-01 Published:2009-02-01
  • Contact: QIAO Hai-yan

安全协议的测试与证明

乔海燕   

  1. 中山大学,广州 510275
  • 通讯作者: 乔海燕

Abstract: 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.

Key words: testing, Needham-Schroeder-Lowe(NSL) protocol, functional programming

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

关键词: 测试, Needham-Schroeder-Lowe协议, 函数程序设计