利用逻辑方法对密码协议进行分析时，从协议描述的用户会话消息出发，在初始假设的基础上，利用逻辑公理，通过一系列推理，证明协议是否满足安全属性，如图所示。

密码协议形式逻辑分析原理

逻辑分析法又称逻辑推理法，起源于Burrows、Abadi和Needham提出的BAN逻辑，BAN逻辑将体现信念的认知模态逻辑用于安全协议的分析，其中协议主体的信念被描述为一组公式，新的信念可由一组推理规则可从原有的信念得到。BAN逻辑的语法区分为3种密码要素：主体、密钥和时鲜值，协议的每个消息表达为该逻辑的1个公式。假设和代表参与协议的主体，代表密钥，和是公式，逻辑的基本公式形式及含义如下：

表示相信，相信真；

表示看见，曾经收到过包含的消息并读到了；

表示曾经说过，曾经发过过包含的消息；

表示可以裁定，信任对于的真值的判定；

表示是新鲜的，在当前协议运行前没有被发送过；

表示和共享一个好的密钥；

表示具有密钥，相应的私钥只有和他信任的人知道；

表示和共享秘密；

表示用加密后的消息；

表示与公式的结合。

BAN逻辑的推导规则直观的反映了逻辑公式构造的语义。定义逻辑公式成立则成立，记为：

BAN逻辑包含以下推理规则：

①消息意义规则:

②公钥意义规则:

③新鲜性规则:

④时鲜值验证规则:

⑤裁定规则:

BAN逻辑直观、易用且应用广泛。为补足BAN逻辑的局限性，随后提出了GNY逻辑、AT逻辑、SVO逻辑等BAN类逻辑。此外，为满足不同密码属性和应用环境的需求，完善逻辑分析方法，又提出了适用于电子商务的Kailar逻辑和验证时间相关的CS逻辑。以上密码协议逻辑可靠性建立在逻辑语义上，要保证计算可靠性，需要建立计算语义，CPCL、IK逻辑和计算不可区分逻辑(CIL)便是均为具备计算可靠性的密码协议逻辑分析方法。由于逻辑分析方法难以完全反映协议运行的全貌，应用背景兼容性局限，分析结果相对不够准确，逻辑分析方法研究已经不能成为唯一准确分析密码协议的方法。