3.8.3  支付协议认证

假设只有那些能够忠实遵守协议的可信主体拥有密钥K，那么形式化认证就很直截了当。方法是从想得到的结果出发反向推理。本例中，我们需要证明零售商信任这张支票，也就是证明R|≡X(从这个角度可以认为支票和密钥的语法是类似的，即当且仅当支票真实并且其上的日期距今很近时才有效)。

现在要用裁定规则推导出R|≡X，需要的条件为R|≡C|X(R相信C有裁定X的资格)和R|≡C|≡X(R认为C相信X)。

第一个条件符合硬件约束，即只有C才能发出形如{C,…}K的文本。

第二个条件R|≡C|≡X必须用Nonce认证规则推导，需要的条件为#X(X是新鲜的)和R|≡C|～X (R相信C发出的X)。

#X是由出现在包括序列号NR的{C，NC，R，NR，X}K中的X推导出来的，而R|≡C|～X是从硬件约束中得到的。

上面给出的是证明摘要，包含必要的信息，且相当简洁。如果需要理解有关身份验证的逻辑细节，可以查找原文[48]，并参阅本章末尾处推荐的更多读物。

3.8.4  形式化认证的局限性

在安全协议设计中，形式化方法是可以用于发现bug的优秀方法，这是因为形式化方法迫使设计者把每个情况都进行显式的表述，从而面临困难的设计选择，否则就无法通过形式化认证。然而，形式化方法也有其局限性。

第一个问题是我们所做的外部假设。比如，我们假设未经授权使用密钥的人无法拿到密钥，而实际上这个假设并不总成立。尽管我们的钱包协议是在防篡改的智能卡上执行的，但是其软件会存在漏洞，并且，任何情况下所提供的防篡改性都不可能是完整的(第16章将讨论这一问题)。因此系统使用了很多回退机制来检测和抵制假卡，比如“影子账号”，它跟踪每张卡上应有的余额并在每次交易完成后刷新，其中还列出了发送到各个终端上的热卡名单，这些措施可以防范被盗用的卡，也可以用来对付假卡。

第二个问题是，协议的理想化经常存在很多问题。在这一系统的早期版本中，就有一个有趣的缺陷。密钥K实际上由两个密钥组成：首先用一个“交易密钥”加密，这个密钥是多变的(就是说，每张卡都有自己的变种)，之后再用一个“银行密钥”加密，这个密钥是不变的。第一次加密由网络操作员完成，第二次加密在该卡的发卡银行完成。这样做的目的是为了实现双重控制，以确保即便攻击者成功地从一张卡上找出了密钥，也只能伪造这一张卡，而无法伪造其他卡(从而击溃热卡机制)。但是由于银行的密钥是不变的，任何攻击者只要解开了一张卡就知道了这个密钥。这意味着攻击者可以解开加密的外部包装，由此，在某些环境下，进行消息重放攻击是可能的(在攻击者发现和利用这个漏洞之前，后来的版本中银行密钥就已经是多变的了)。

在这个例子中形式化认证方法并没有失败，因为没有试图对多样机制进行确认。但是它确实阐述了安全工程中的一个普遍问题——?漏洞出现在两种保护技术的边界处。本例中有三种技术：硬件防篡改、身份验证协议和影子账号/热卡黑名单机制。不同领域的专家通常会使用不同的保护技术，而他们并不完全了解别人所作的假设(这也是安全工程师需要本书这类书籍的原因之一：帮助各学科专家去了解彼此的工具并进行更有效的沟通)。

鉴于以上原因，人们已经研究了其他替代方法来确保身份验证协议的设计，其中包括协议鲁棒性(protocol robustness)思想。正如结构化编程技术的目标是确保系统化地设计软件而不遗漏任何要点，鲁棒性协议设计的目标主要是为了明晰。鲁棒性原则包括：一个协议的阐述只应该依据它的内容，而不是其上下文；每个要素(比如主体的名称)都应该在消息中显式声明。还有一些问题涉及序列号、时间戳和随机质询提供的新鲜性以及加密方式。如果协议中采取了公钥密码学或者数字签名机制，还有更多的技术鲁棒性问题。