安全协议的测试与证明

摘要

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