基于ProVerif的安全攻击仿真+源代码(4)
1.2.2 安全协议形式化分析方法的分类
安全协议形式化分析方法主要分为以下几类[4,5,10,11,12]：模态逻辑方法、模型检测方法、定理证明方法。
(1)模态逻辑。由一些推理规则组成命题，表示主体对消息的知识或信仰，运用推理规则可以从已知的知识和信仰推导出新的知识和信仰。模态逻辑方法主要包含以BAN逻辑、类 BAN逻辑。BAN逻辑是最早的以逻辑形式提出的方法，它的一个重要特点是简单直观、易于掌握。但是，BAN 逻辑还存在语义的不完备等问题。后来，许多研究以 BAN 逻辑为基础，通过一定的改进或扩展，提出了新的逻辑方法--BAN 类逻辑。BAN 类逻辑因其简单、直观、易用性而受到很多人的欢迎。