总述
BAN(Burrows, Abadi, and Needham)逻辑是一种基于信念的模态逻辑，在BAN逻辑的推理过程中，参加协议的主体的信念随消息交换的发展，不断变化和发展。应用BAN逻辑时，首先需要进行理想化步骤，将协议的消息转换为BAN逻辑中的公式，在根据具体情况进行合理假设，由逻辑的推理规则根据理想化协议和假设进行推理，推断协议能否完成预期目标。
BAN逻辑中的假设
BAN逻辑在抽象的层次上讨论认证协议的安全性，其为协议的分析和正确性验证提供了形式化的方法，是一个重要的工具。但它并不考虑由协议的具体实现所带来的安全缺陷和由于加密体制的缺点所引发的协议缺陷。
BAN逻辑系统所做的假设如下：
密文块不能被篡改，也不能用几个小的密文块组成一个新的大密文块一个消息中的两个密文块被看作是分两次分别到达的总假设加密系统是完善的，即只有掌握密钥的主体才能理解密文消息。因为不知道密钥的主体，不能解密密文而得到明文。攻击者无法从密文推断出密钥密文含有足够的冗余信息，使解密者可以判断他是否应用了正确的密钥消息中含有足够的冗余信息，使主体可以判断该消息是否来源于自身假设参与协议的主体是诚实的
符号表示
BAN逻辑主要包含3种处理对象：主体(principal)，密钥(keys)和公式(formula)。其中公式也称为语句或命题(statement)。BAN逻辑仅包合取这一命题连接词，用逗号表示，合取连接词满足交换律和结合律。
依照BAN逻辑的惯例，P，Q，R表示主体变量，K表示密钥变量，X和Y表示公式变量。此外，若K表示公钥，则K的逆元表示与之对应的私钥。
BAN逻辑的10个构件(语法和语义)
，表示主体P相信公式X是真的（或 P believes X），表示主体P接收到了包含X的消息，即存在某主体Q向P发送了包含X的消息（或 P sees X），表示主体P曾经发送过包含X的消息（或 P said X），表示主体P对X有管辖权（或 P controls X），表示X是新鲜的，即X没有在当前回合前作为某消息的一部分被发送过，这里X一般为临时值（或 fresh(X)），表示K为P和Q之间的共享密钥，且除P与Q以及他们相信的主体之外，其他主体都不知道K 或 ，表示K为P的公开密钥，且除P和他相信的主体之外，其他主体都不知道相应的秘密密钥，表示X为P和Q的共享秘密，且除P和Q以及他们相信的主体之外，其他主体都不知道X，表示用密钥K加密X后得到的密文，这是 的缩写，表示由X和秘密Y合成的消息
BAN逻辑的19条推理规则
注： 表示元语言符号， 表示可以由前提集A推导出结论C
消息含义规则(message-meaning rules) 3条：
临时值验证规则(nonce-verification rule) 1条：
管辖规则(jurisdiction rule) 1条：
接收消息规则(seeing rules) 5条
消息新鲜性规则(freshness rule) 1条
信念规则(belief rules) 4条
密钥与秘密规则(key and secret rules) 4条