| 摘要: |
| 加密协议的分析需要形式化的方法和工具.该文定义了加密协议描述语言PEP (principals+environment=protocol),并说明对于一类加密协议,其PEP描述可以转化为有穷的基本CCS进程,由此可以在基于CCS的CWB(concurrency workbench)工具中分析加密协议的性质.此方法的优点在于隐式地刻画攻击者的行为,试图通过模型检查(model checking)发现协议潜在的安全漏洞,找到攻击协议的途径. |
| 关键词: 加密协议,协议分析,形式化方法,CCS,模型检查. |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家自然科学基金 |
|
| CCS-based Cryptographic Protocol Analysis |
|
DING Yi-qiang
|
| Abstract: |
| Formal methods and tools are key aspects for the analysis of cryptographic protocols. In this paper, a formal language PEP (principals+environment=protocol) for the specification of cryptographic protocols is proposed. For some cryptographic protocols, their PEP specifications can be translated into finite basic CCS processes, so it is possible to analyze the security properties using CCS-based tools such as CWB (concurrency workbench). The advantage of the mothod proposed in this paper is that the actions of the attacker can be implicitly specified, and if the potential back door of the protocol analyzed exists, the attacking action trace can be explicitly found out by model checker. |
| Key words: Cryptographic protocols, protocol analysis, formal methods, CCS, model checking. |
