Abstract: This paper researches on quick and efficient formal analysis of security protocol, and presents the concept of trust domain. Diagrammatic analysis is adopted, which makes deduction of protocol more clear and intuitive. This method analyzes the trust domain of protocol entity directly, which makes analysis easier. Experimental results show that the method is faster and more intuitive compared with traditional methods. It provides ways and basis for finding redundancies of security protocols.

Key words: formal analysis, security protocol, BAN logic, NSSK protocol

摘要： 对快速、高效的形式化分析安全协议进行研究，提出“信任域”的概念。采用与图形化相结合的分析方法，使得协议流程的推导过程清晰、直观。该方法直接分析协议参与主体的信任域，简化分析过程和步骤。实验结果表明，与传统方法相比，该方法更快速、直观，并能为分析协议的冗余性提供具体方法和依据。

关键词: 形式化分析, 安全协议, BAN逻辑, NSSK协议

CLC Number: 

• TP309