BAN逻辑只在抽象的层次上讨论密码协议的安全性，因此它不考虑由协议的具体实现所带来的安全缺陷和由于加密体制的缺点所引发的协议缺陷。总的来说，BAN逻辑系统所做的假设如下。

（1）密文块不能被篡改，也不能用几个小的密文块组成一个新的大密文块。

（2）一个消息中的两个密文块被看作是分两次分别到达的。

（3）总假设加密系统是完善的，即只有掌握密钥的主体才能理解密文消息，因为不知道密钥的主体不能解密得到明文，攻击者无法从密文推断出密钥。

（4）密文含有足够的冗余信息，使解密者可以判断他是否应用了正确的密钥。

（5）BAN逻辑还假设参与协议的主体是诚实的。

作为一种多类型模态逻辑，BAN逻辑主要包含下面3种处理对象：主体、密钥和公式，公式也称为语句或命题。协议的每个消息表达为该逻辑的一个公式。假设P、Q、R、R′代表一般意义上的主体，A、B、C代表具体的认证主体，S代表可行第三方，IDA代表主体A的身份标识，KAB、KAS、KBS代表具体认证主体的共享密钥，KA、KB、KC代表具体认证主体的公开密钥，K-1A、K-1B、K-1C代表具体认证主体，K代表一般意义上的加密密钥，NA、NB、NC代表具体的观点（如随机数），X、Y是一般意义上的消息。逻辑的基本公式及其语义可以用表12.1表示。

表12.1　BAN逻辑的基本公式及其语义

(www.daowen.com)

BAN的推导规则直观地反映了逻辑公式构造的语义，我们把“逻辑公式X1，X2，…，Xn成立则Y成立”记为

下面是BAN的19条推理规则。

（1）消息含义规则

①共享密钥情况