学术上的教训
在前面的协议中，那些被破译的协议和没有被破译的协议都有一些重大的教训：
- 因为设计者试图设计得太精巧，许多协议失败了。他们通过省去重要的部分：名字、随机数等等来优化他们的协议， 但矫枉过正了[43，44]。
- 试图优化绝对是一个可怕的陷阱，并且全部命运依赖于你所做的假设。例如：如果你有识别的时间，你就可以做许许多多你没去做也做不到的事情。
- 选择的协议依赖于底层的通信体系结构。你难道不想使消息的大小和数量最小吗？是团体中的所有人都能够互相交谈呢？还是只有他们中的几个人能够交谈？
类似这些问题导致了协议分析的形式化方法的开发。
3.4 鉴别和密钥交换协议的形式分析
在网络上的一对计算机（和人）之间建立安全的会话密钥问题是如此的重要，以至于引发出许多研究。一些研究着重开发协议， 例如开发3.1节、3.2节、3.3节中讨论的那些协议。这又导致了更大和更多有趣的问题：鉴别和密钥交换协议的形式分析。在提出似乎是安全的协议的以后岁月里，人们发现了这些协议的缺陷，研究人员想要得到从一开始就能证明协议的安全性各种工具。虽然很多这种工作都能应用到一般的密码协议中去，但是研究的重点却毫无例外地放在鉴别和密钥交换上。
对密码协议的分析有四种基本途径[1045]：
1．使用规范语言和验证工具建立协议模型和验证协议，它不是特别为密码协议分析设计的。
2．开发专家系统，协议设计者能够用它来调查研究不同的情况。
3．用分析知识和信任的逻辑，建立协议族的需求模型。
4．开发形式化方法，它基于密码系统的代数重写项性质。
关于这四种途径的所有讨论和围绕它们的研究远远超出了本书的范围。文献[1047，1355]对这个题目作了很好的介绍。我只略微谈到这个领域的主要作用。
第一种途径把密码学协议当作任何其他计算机程序对待，并试图证明它的正确性。一些研究者把协议表示为有限状态机[1449，1565]，其他人使用一阶判定微积分[822]，还另有一些人使用规范语言来分析协议[1566]。然而证明正确性与证明安全性不同，并且这个方法对于发现许多缺陷的协议来说是行不通的。虽然这一种途径最早被广泛研究，但这个领域的大多数工作已经转向获得普及的第3种途径。
第二种途径是使用专家系统来确定协议是否能达到不合乎需要的状态（例如密钥的泄露）。虽然这种途径能够更好地识别缺陷，但它既不能保证安全性，又不能为开发攻击提供技术。它的好处在于决定协议是否包含已知的缺陷，但不可能发现未知的缺陷。这种途径的例子可在[987，1521]中找到。[1092]讨论了一个由美国军方开发的基于规则的系统，这个系统叫做询问器。
第三种途径到目前为止是最流行的，它是由Michael Burrows、Martin Abadi和Roger Needham首先发明的。为了进行知识和信任分析，他们开发了一个形式逻辑模型，叫做BAM逻辑[283，284]。BAM逻辑是分析鉴别协议时用得最广泛的逻辑。它假设鉴别是完整性和新鲜度的函数，并使用逻辑规则来对贯穿协议的那些属性的双方进行跟踪。虽然已经提出了这种途径的许多变化和扩展，但大多数协议设计者仍在引用最初的研究。
BAM逻辑并不提供安全性证明，它只能推出鉴别。它具有容易使用的简单、明了的逻辑，对于发现缺陷仍然有用。BAM逻辑中的一些命题有：
Alice 相信X（Alice装作好像X是正确的）。
Alice看X（某些人已经把包含X的消息发给Alice，Alice可能在解密消息后，能够读和重复X）。
Alice说X（在某一时间，Alice发送包括命题X的消息。不知道的是，消息在多早以前曾被发送过，或是在协议当前运行期间发送的。已经知道，当Alice说X时，Alice相信X。）
X是新的（在当前运行协议以前，X在任何时间没有把消息发送出去）等等。 BAM逻辑也为协议中有关信任理由提供规则。这些规则能够用到协议的逻辑命题，用来证明事情或回答有关协议的问题。例如，消息内涵的规则是：
如果Alice相信Alice和Bob共享秘密密钥K，Alice看见用K加密的X，而Alice没有用K加密X，那么Alice相信Bob曾经说过X。
另一个规则是只以当时为限的验证规则：
如果Alice相信X只在最近被发送，并且Bob曾经说过X，那么Alice就认为Bob相信X。
用BAM逻辑进行分析分四步：
（1）采用以前描述的命题，把协议转换为理想化形式。
（2）加上有关协议初始状态的所有假设。
（3）把逻辑公式放到命题中：在每个命题后断言系统的状态。
（4）为了发现协议各方持有的信任，运用逻辑基本原理去断言和假设。
BAM逻辑的作者“把理想化的协议看作比在文献中发现传统的描述更清楚和更完善的规范…”[283，284]。其它协议没有这种印记，并因为它不可能正确地反映实际的协议而批评这个步骤[1161，1612]。在[221，1557]中有进一步的争论。其它批评试图表明，BAM逻辑可能推导出关于协议明显错误的特征[1161]，见[285，1509]的辩驳。并且BAM逻辑只涉及信任，而与安全性无关[1509]。在[1488，706，1002]中有更多这方面的争论。
尽管有这些批评，BAM逻辑仍是成功的。它已经在几种协议中发现缺陷，这些协议包括Needham-Schroeder 和一个早期CCITT X。509协议草案[303]。它已经发现很多协议中的冗余，这些协议包括Yahalom、Needham-Schroeder和Kerberos。许多人的文章使用BAM逻辑，声称他们协议的安全性[40，1162，73]。
其它逻辑系统也有公布，一些设计成为BAM逻辑的扩展[645，586，1556，828]，另一些是基于BAM逻辑去改进发现的弱点[1488，1002]。虽然GNY有一些缺点[40]，但它是这些当中最为成功的一个[645]。文献[292，474]提出应将概率信任加到BAM逻辑中去，以配合成功，在[156，798，288]讨论了其它形式逻辑，[1514]试图把几个逻辑的特点结合起来，[1124，1511]提出了信任能够随时间而改变的逻辑。
密码协议分析的第四种途径是把协议当作一个代数系统模型，表示有关协议参与者了解的状态，然后分析某种状态的可达性。这种途径没有像形式逻辑那样引起更多的注意，但情况正在改变。它首先由Michael Merritt使用[1076]，他证明代数模型可用来分析密码协议。其它途径在[473，1508，1530，1531，1532，1510，1612]中描述。
海军研究试验室（NRL）的协议分析器可能是这些技术中最成功的应用[1512，823，1046，1513]；它被用来在各种协议中寻找新的和已知的缺陷[1044，1045，1047]。这台协议分析器定义了下面的行为：
- 接收（Bob，Alice，M，N）。（Bob在N地附近，接收消息M作为来自Alice的消息。）
- 获悉（Eve，M）。（Eve获悉M。）
- 发送（Alice，Bob，Q，M）。（根据查询Q，Alice发送M给Bob。）
- 请求（Bob，Alice，Q，N）。（Bob在N地附近，发送Q给Alice。）
从这些行为中，可以确定需求。例如：
- 如果Bob在过去某些点接收到从Alice来的消息M，那么Eve在过去某些点没有获悉M。
- 如果Bob在他的N地附近接收到从Alice来的消息M，Alice给Bob发送M作为Bob在N地附近查询的响应。
为了使用NRL协议分析器，必须按以前的结构规定协议。分析有四个步骤：À为诚实的参与者定义传送；Á描述对所有诚实和不诚实参与者可得到的操作；Â描述基本的协议构造部件；Ã描述还原规则。这里表示的所有要点是已知的协议要与它的需求相符。采用像NRL协议分析器这样的工具，最终会产生一个能够证明是安全的协议。