安全协议的形式化分析技术方法研究

安全协议是解决网络安全问题最有效的手段之一。然而,由于互联网的开放性和协议的并发性,安全协议的设计和分析一直是一个复杂而困难的问题。实践证明,借助形式化的方法或工具分析安全协议是非常必要而且行之有效的。安全协议的形式化分析已有三十多年的历史,一直存在两类不同的方法:计算方法和符号方法。符号方法用形式化语言和符号推理对协议进行分析和验证,更容易实现自动化分析。但是由于对密码学原语和攻击者能力的理想建模,使得这类分析方法的肯定性结论往往并不直接具有现实意义,被认为没有真正建立起密码学的可靠性。