Abstract: In order to analyze the authentication protocols and find attacks effectively, a formal method based on message matching is introduced. It uses strand spaces to model the protocols and analyzes possible roles the attackers can act. Based on the rules of protocols, this method assigns variants and matches constants in message and knowledge set step by step. It can utilize authentication test to reduce the scope of analysis and find the attack traces as a result. In addition, this method provides the guidance to modify the authentication protocols.

Key words: message matching, strand spaces, knowledge set, authentication test

摘要： 为了有效地分析和验证认证协议的安全性，找出协议的漏洞，介绍一种基于消息匹配的形式化分析方法。利用串空间对协议进行建模，吸取模型检测的思想，分析攻击者可能扮演的角色以及协议的执行规则，在此基础上逐步给消息和主体知识集中的变量进行赋值，并匹配消息中已被确定的常量，以此找出具体的攻击路径。同时，结合认证测试方法简化分析步骤，针对分析过程对协议进行有效的改进。

关键词: 消息匹配, 串空间, 知识集, 认证测试

CLC Number: 

• TP393.08