形式化方法兴起于20世纪70年代末期，如今已广泛用于解决理论和实际问题，计算机安全是一个它比较成功的应用领域。

形式化的数学系统是一个由符号以及使用这些符号的规则共同组成的系统。规则可以是形成规则（规定构成正确形式公式符号的字符串）、证明规则（规定构成证明公式的字符串）或者语义规则（把公式映射到一个代数域）。形式化方法是将概念或方法经过高度抽象后使用一定的数学模型进行表示，通过推演计算来研究数学模型，进而揭示概念和方法的内在规律的研究方法。

形式化方法广泛应用于安全模型分析、流分析、安全协议分析、软件验证、硬件验证、体系结构分析、秘密信道分析等。

形式化方法在安全学界最大的成功是应用它分析安全协议。安全协议足够小，易于完成形式化分析，而且这些分析发现了很多以前不为人所知的漏洞。就其自身而言，形式化分析技术是有局限性的，协议系统的运行不是独立的，而是处于某种环境之下。系统的形式化说明是基于对系统环境的某种假设之上的。只有当假设成立时，证明才成立。所以，一旦某种假设不成立，一切证明就无从谈起，而入侵者只要违反了系统的假设，就可成功入侵系统。而且，即便明确给出假设的详细说明，也不可避免地会遗漏一些情况。

安全协议的形式化分析至少可以完成以下工作：

（1）界定协议运行系统的边界；

（2）更加准确地描述系统的行为；(www.daowen.com)

（3）更准确地定义系统的特性；

（4）证明系统在特定的假设前提下满足一定的特性。

安全协议的形式化分析方法是采用各种形式化的语言或者模型，为安全协议建立模型，并按照规定的假设和分析、验证方法证明协议的安全性。图12.1给出了安全协议的形式化验证过程。

从图12.1中可以看出，为了对一个安全协议进行形式化分析，首先要将协议的非形式化描述（如RFC文档）转换为形式化的规范说明，然后结合协议的入侵者模型，将两者作为形式化分析工具的输入，经过分析工具的处理，最后得到结论。

图12.1　安全协议的形式化验证过程