3.8  邁向形式化

我們已經(jīng)看到，上面討論的協(xié)議中都遇到了一些困難，很多保護機制也依賴于協(xié)議設(shè)計者制定的、可能出錯的(或后來被誤解)初始假設(shè)，這些問題使得研究人員在密鑰分配協(xié)議中采用形式化方法。最初，形式化方法的目的是為了判斷協(xié)議是否正確：或者可以被證明是正確的，或者可以用攻擊測試來證明正確性。最近，形式化方法已經(jīng)擴展到用于闡明協(xié)議的各種基本假設(shè)。

有大量方法可以證明協(xié)議的正確性，最著名的一種方法是信任邏輯(logic of belief)，也稱為BAN邏輯，它是以發(fā)明者Burrows、Abadi和Needham的名字命名的［249］。該邏輯可以在已知消息和時間戳等條件時，推斷出主體應該信任什么。另一種方法是隨機預言模型(random oracle model)，這將在第5章提到。很多致力于密碼學理論研究的研究者對這一模型都很感興趣，這種方法在表達能力上不如信任邏輯，但可將協(xié)議屬性與底層加密算法屬性綁定在一起。最后，很多研究者采用了主流的形式化方法，比如CSP以及Isabelle等認證工具。

歷史上，有些用形式化方法證明無誤的協(xié)議中實際上存在缺陷，下一節(jié)給出了一個典型的示例。

3.8.1  一個典型的智能卡銀行協(xié)議

COPAC是VISA在電信基礎(chǔ)設(shè)施較差的國家中使用的一種電子錢包系統(tǒng)[48]，它是底層協(xié)議使用形式化技術(shù)(BAN邏輯的變種)進行設(shè)計和驗證的，是最早投入使用的金融系統(tǒng)。與其類似的一個協(xié)議現(xiàn)在還應用在Geldkarte中，這是德國銀行向客戶發(fā)行的一種電子錢包，法國的銀行業(yè)也采用了這個協(xié)議(稱為Moneo)，比利時的類似系統(tǒng)則稱為Proton。歐洲的應用集中于低額的交易，比如停車計時器與售貨機等設(shè)備，這種情況下使用網(wǎng)絡(luò)連接是不經(jīng)濟的。

交易發(fā)生在客戶智能卡和商店智能卡(在投幣式自動售貨機的情況下，此智能卡存放在機器中，并在重新補貨后改變)之間。顧客給商店一張電子支票，內(nèi)含兩個身份驗證碼，一個可以通過網(wǎng)絡(luò)進行核對，另一個由客戶的銀行核對。該協(xié)議可以簡要描述如下：

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以及剛剛從顧客那里收到的信息；之后，顧客發(fā)出電子支票X和迄今為止協(xié)議中已交換的全部數(shù)據(jù)。對電子支票，可以將其看做需要顧客和零售商的賬號及其各自引用號的一種支付設(shè)備(在每條消息中都重復前面的所有數(shù)據(jù)，這樣做的目的是防止攻擊者使用“剪切-粘貼”方式進行消息操縱攻擊)。