认证协议的形式化描述及其安全性分析是安全协议形式化分析的关键问题之一.为了解决以往分析方法中协议规范形式化描述存在的问题,提出了一种协议规范有向图描述方法,并在此基础上提出了协议消息构造的逆向搜索算法.用该算法分析Woo-Lam认证协议,找到了该协议一种新的攻击方法及其攻击路径.
The formal description of authentication protocol and its security analysis are one of the most important issues in the protocol analysis. In order to solve the problems in the formal description of cryptographic protocol, a method based on directed graph is presented to formally depict the authentication protocol specification. Meanwhile, a converse-searching algorithm based on directed graph is also presented to construct the protocol messages. Woo-Lam Authenticate protocol is analyzed with this method, and a new flow and its attacking trace are founded.