论文部分内容阅读
逻辑方法和模型检验方法是安全协议的两种重要分析方法。逻辑方法简单、直观，但其最大问题是不够完备，模型检验方法自动化程度高且能生成不满足所需求性质的反例。先用BAN逻辑对Andrew Secure RPC协议进行分析，并在此基础上组合模型检验方法进行分析，结果表明逻辑方法组合模型检验方法分析协议比只用逻辑方法分析得到的结果更全面且更具体。