3.8.3  支付協(xié)議認證

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

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

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

第二個條件R|≡C|≡X必須用Nonce認證規(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是從硬件約束中得到的。

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

3.8.4  形式化認證的局限性

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

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

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

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

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