Andrew Secure RPC协议的一种组合分析方法

A Combined Analysis Method of Andrew Secure RPC Protocol

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

Logic and model checking are two important analysis methods of security protocols.Logic is simple and visual but it is not complete enough.Model checking has high automation and can generate counter examples which do not satisfy the properties needed.In the paper,Andrew Secure RPC protocol is firstly analyzed by BAN logic,then it is analyzed by model checking on the base.The result shows that compared with logic method,the combined method can get more overall and more specific results.