3.8  迈向形式化

我们已经看到，上面讨论的协议中都遇到了一些困难，很多保护机制也依赖于协议设计者制定的、可能出错的(或后来被误解)初始假设，这些问题使得研究人员在密钥分配协议中采用形式化方法。最初，形式化方法的目的是为了判断协议是否正确：或者可以被证明是正确的，或者可以用攻击测试来证明正确性。最近，形式化方法已经扩展到用于阐明协议的各种基本假设。

有大量方法可以证明协议的正确性，最著名的一种方法是信任逻辑(logic of belief)，也称为BAN逻辑，它是以发明者Burrows、Abadi和Needham的名字命名的［249］。该逻辑可以在已知消息和时间戳等条件时，推断出主体应该信任什么。另一种方法是随机预言模型(random oracle model)，这将在第5章提到。很多致力于密码学理论研究的研究者对这一模型都很感兴趣，这种方法在表达能力上不如信任逻辑，但可将协议属性与底层加密算法属性绑定在一起。最后，很多研究者采用了主流的形式化方法，比如CSP以及Isabelle等认证工具。

历史上，有些用形式化方法证明无误的协议中实际上存在缺陷，下一节给出了一个典型的示例。

3.8.1  一个典型的智能卡银行协议

COPAC是VISA在电信基础设施较差的国家中使用的一种电子钱包系统[48]，它是底层协议使用形式化技术(BAN逻辑的变种)进行设计和验证的，是最早投入使用的金融系统。与其类似的一个协议现在还应用在Geldkarte中，这是德国银行向客户发行的一种电子钱包，法国的银行业也采用了这个协议(称为Moneo)，比利时的类似系统则称为Proton。欧洲的应用集中于低额的交易，比如停车计时器与售货机等设备，这种情况下使用网络连接是不经济的。

交易发生在客户智能卡和商店智能卡(在投币式自动售货机的情况下，此智能卡存放在机器中，并在重新补货后改变)之间。顾客给商店一张电子支票，内含两个身份验证码，一个可以通过网络进行核对，另一个由客户的银行核对。该协议可以简要描述如下：

C→R： {C,NC}K

R→C： {R,NR,C,NC}K

C→R： {C,NC,R,NR,X}K

用自然语言描述如下：顾客和零售商共享密钥K，顾客使用这个密钥对含有其账号C和客户交易序列号NC的消息加密，零售商确认自己的账号R、交易序列号NR以及刚刚从顾客那里收到的信息；之后，顾客发出电子支票X和迄今为止协议中已交换的全部数据。对电子支票，可以将其看做需要顾客和零售商的账号及其各自引用号的一种支付设备(在每条消息中都重复前面的所有数据，这样做的目的是防止攻击者使用“剪切-粘贴”方式进行消息操纵攻击)。