3.8  邁向形式化

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

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

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

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

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

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

C→R： {C,NC}K

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

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

用自然語(yǔ)言描述如下：顧客和零售商共享密鑰K，顧客使用這個(gè)密鑰對(duì)含有其賬號(hào)C和客戶交易序列號(hào)NC的消息加密，零售商確認(rèn)自己的賬號(hào)R、交易序列號(hào)NR以及剛剛從顧客那里收到的信息；之后，顧客發(fā)出電子支票X和迄今為止協(xié)議中已交換的全部數(shù)據(jù)。對(duì)電子支票，可以將其看做需要顧客和零售商的賬號(hào)及其各自引用號(hào)的一種支付設(shè)備(在每條消息中都重復(fù)前面的所有數(shù)據(jù)，這樣做的目的是防止攻擊者使用“剪切-粘貼”方式進(jìn)行消息操縱攻擊)。