3.8.3  支付協(xié)議認(rèn)證

假設(shè)只有那些能夠忠實(shí)遵守協(xié)議的可信主體擁有密鑰K，那么形式化認(rèn)證就很直截了當(dāng)。方法是從想得到的結(jié)果出發(fā)反向推理。本例中，我們需要證明零售商信任這張支票，也就是證明R|≡X(從這個(gè)角度可以認(rèn)為支票和密鑰的語法是類似的，即當(dāng)且僅當(dāng)支票真實(shí)并且其上的日期距今很近時(shí)才有效)。

現(xiàn)在要用裁定規(guī)則推導(dǎo)出R|≡X，需要的條件為R|≡C|X(R相信C有裁定X的資格)和R|≡C|≡X(R認(rèn)為C相信X)。

第一個(gè)條件符合硬件約束，即只有C才能發(fā)出形如{C,…}K的文本。

第二個(gè)條件R|≡C|≡X必須用Nonce認(rèn)證規(guī)則推導(dǎo)，需要的條件為#X(X是新鮮的)和R|≡C|～X (R相信C發(fā)出的X)。

#X是由出現(xiàn)在包括序列號NR的{C，NC，R，NR，X}K中的X推導(dǎo)出來的，而R|≡C|～X是從硬件約束中得到的。

上面給出的是證明摘要，包含必要的信息，且相當(dāng)簡潔。如果需要理解有關(guān)身份驗(yàn)證的邏輯細(xì)節(jié)，可以查找原文[48]，并參閱本章末尾處推薦的更多讀物。

3.8.4  形式化認(rèn)證的局限性

在安全協(xié)議設(shè)計(jì)中，形式化方法是可以用于發(fā)現(xiàn)bug的優(yōu)秀方法，這是因?yàn)樾问交椒ㄆ仁乖O(shè)計(jì)者把每個(gè)情況都進(jìn)行顯式的表述，從而面臨困難的設(shè)計(jì)選擇，否則就無法通過形式化認(rèn)證。然而，形式化方法也有其局限性。

第一個(gè)問題是我們所做的外部假設(shè)。比如，我們假設(shè)未經(jīng)授權(quán)使用密鑰的人無法拿到密鑰，而實(shí)際上這個(gè)假設(shè)并不總成立。盡管我們的錢包協(xié)議是在防篡改的智能卡上執(zhí)行的，但是其軟件會存在漏洞，并且，任何情況下所提供的防篡改性都不可能是完整的(第16章將討論這一問題)。因此系統(tǒng)使用了很多回退機(jī)制來檢測和抵制假卡，比如“影子賬號”，它跟蹤每張卡上應(yīng)有的余額并在每次交易完成后刷新，其中還列出了發(fā)送到各個(gè)終端上的熱卡名單，這些措施可以防范被盜用的卡，也可以用來對付假卡。

第二個(gè)問題是，協(xié)議的理想化經(jīng)常存在很多問題。在這一系統(tǒng)的早期版本中，就有一個(gè)有趣的缺陷。密鑰K實(shí)際上由兩個(gè)密鑰組成：首先用一個(gè)“交易密鑰”加密，這個(gè)密鑰是多變的(就是說，每張卡都有自己的變種)，之后再用一個(gè)“銀行密鑰”加密，這個(gè)密鑰是不變的。第一次加密由網(wǎng)絡(luò)操作員完成，第二次加密在該卡的發(fā)卡銀行完成。這樣做的目的是為了實(shí)現(xiàn)雙重控制，以確保即便攻擊者成功地從一張卡上找出了密鑰，也只能偽造這一張卡，而無法偽造其他卡(從而擊潰熱卡機(jī)制)。但是由于銀行的密鑰是不變的，任何攻擊者只要解開了一張卡就知道了這個(gè)密鑰。這意味著攻擊者可以解開加密的外部包裝，由此，在某些環(huán)境下，進(jìn)行消息重放攻擊是可能的(在攻擊者發(fā)現(xiàn)和利用這個(gè)漏洞之前，后來的版本中銀行密鑰就已經(jīng)是多變的了)。

在這個(gè)例子中形式化認(rèn)證方法并沒有失敗，因?yàn)闆]有試圖對多樣機(jī)制進(jìn)行確認(rèn)。但是它確實(shí)闡述了安全工程中的一個(gè)普遍問題——?漏洞出現(xiàn)在兩種保護(hù)技術(shù)的邊界處。本例中有三種技術(shù)：硬件防篡改、身份驗(yàn)證協(xié)議和影子賬號/熱卡黑名單機(jī)制。不同領(lǐng)域的專家通常會使用不同的保護(hù)技術(shù)，而他們并不完全了解別人所作的假設(shè)(這也是安全工程師需要本書這類書籍的原因之一：幫助各學(xué)科專家去了解彼此的工具并進(jìn)行更有效的溝通)。

鑒于以上原因，人們已經(jīng)研究了其他替代方法來確保身份驗(yàn)證協(xié)議的設(shè)計(jì)，其中包括協(xié)議魯棒性(protocol robustness)思想。正如結(jié)構(gòu)化編程技術(shù)的目標(biāo)是確保系統(tǒng)化地設(shè)計(jì)軟件而不遺漏任何要點(diǎn)，魯棒性協(xié)議設(shè)計(jì)的目標(biāo)主要是為了明晰。魯棒性原則包括：一個(gè)協(xié)議的闡述只應(yīng)該依據(jù)它的內(nèi)容，而不是其上下文；每個(gè)要素(比如主體的名稱)都應(yīng)該在消息中顯式聲明。還有一些問題涉及序列號、時(shí)間戳和隨機(jī)質(zhì)詢提供的新鮮性以及加密方式。如果協(xié)議中采取了公鑰密碼學(xué)或者數(shù)字簽名機(jī)制，還有更多的技術(shù)魯棒性問題。