密码协议形式化分析

密码协议形式化分析（formal methods in analythizing cryptographic protocols），理学-计算机科学技术-信息安全-密码学-密码协议-密码协议分析，利用形式化方法分析密码协议安全性的方法。形式化方法通常对所研究问题进行抽象，用数学语言来描述，将问题转化为符号化公式，从而对问题的分析转化为符号化公式的演算或推理，因此形式化方法有时又被称为符号化方法。一般公认，1978年Needham和Schroeder对敌手能力进行抽象和假设，首次提出使用形式化的方法对密码协议进行分析的思想。1981年，Dolev和Yao首次明确给出了一种密码协议形式化分析模型，即Dolev-Yao模型（简称DY模型），并使用该模型对密码协议进行分析，开启了密码协议形式化分析的先河，为随后研究奠定了基础。随后1987年Millen开发最早用于密码协议形式化分析的Interrogator系统，这一系统通过遍历整个状态空间，找到协议安全漏洞，此原理被后来Athena系统沿用。