基于CCS的加密协议分析

摘要

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