一种基于关联规则的安全协议验证方法

Verification method of security protocols based on correlation rules

提出了一种基于关联规则的安全协议形式化分析方法。从主体认证关联、消息间关联和消息内部关联三个角度去刻画协议,提出了基于以上关联特点的协议验证方法。利用该方法对W ooand Lam认证协议进行了逆向验证分析,成功推导出现有的已知攻击路径,使这些已知攻击路径的推导能统一于该验证方法;同时还发现了一个未知的攻击路径,为协议的形式化分析提供了新思路。

An approach for the formal analysis of security protocols based on the correlation rides was proposed. The character of correlation of protocols was pictured from three aspects： the correlation of authentication between principals, the correlation between messages and within the messages. The verification method was presented based on the above correlation property, which had been used to verify the Woo and Lam authentication Protocol in reverse analysis. Some known attack paths were derived successfully, and made these known attack paths can be derived from this method in unity, and also discovered an unknown attack path. The method provides a new perspective in the formal analysis of the protocols.