基于CCS的加密协议分析

CCS-based Cryptographic Protocol Analysis

加密协议的分析需要形式化的方法和工具．该文定义了加密协议描述语言ＰＥＰ（ｐｒｉｎｃｉｐａｌｓ＋ｅｎｖｉｒｏｎｍｅｎｔ＝ｐｒｏｔｏｃｏｌ），并说明对于一类加密协议，其ＰＥＰ描述可以转化为有穷的基本ＣＣＳ进程，由此可以在基于ＣＣＳ的ＣＷＢ（ｃｏｎｃｕｒｒｅｎｃｙｗｏｒｋｂｅｎｃｈ）工具中分析加密协议的性质．此方法的优点在于隐式地刻画攻击者的行为，试图通过模型检查（ｍｏｄｅｌｃｈｅｃｋｉｎｇ）发现协议潜在的安全漏洞，找到攻击协议的途径．

Formal methods and tools are key aspects for the analysis of cryptographic protocols. In this paper, aformal language PEP (principals + environment = protocol ) for the specification of cryptograph is proposed. For some cryptographic protocols, their PEP specifications can be translated into finite basic CCSprocesses, so it is possible to analyze the security properties using CCS-based tools such as CWB (concurrencyworkbench). The advantage of the mothod proposed in this paper is that the actions of the attacker can beimplicitly specified, and if the potential back door of the protocol analyzed exists, the attacking action trace can beexplicitly found out by model checker.