數(shù)據(jù)獨(dú)立技術(shù)在CSP協(xié)議模型中的設(shè)計(jì)

　 從上述定義可以確定這樣的性質(zhì)：如果在明確推理系統(tǒng)中建立攻擊者，并且攻擊者的初始知識(shí)集不包含對(duì)于類型T成員(除了常數(shù)C)的非等價(jià)測(cè)試，那么該進(jìn)程滿足PosConjEqT′c條件(并且因此，整個(gè)協(xié)議模型滿足網(wǎng)絡(luò)其他部分的條件)。

　　可以看出系統(tǒng)成分是否滿足上述性質(zhì)對(duì)研究至關(guān)重要。只有滿足這些條件才能夠在協(xié)議分析的CSP模型中構(gòu)造更為復(fù)雜的事件。

　　(3)Roscoe數(shù)據(jù)獨(dú)立技術(shù)的意義

　　Roscoe在文獻(xiàn)中引入了NM進(jìn)程，負(fù)責(zé)產(chǎn)生系統(tǒng)所需的無(wú)眼新鮮值。那么在以前運(yùn)行中，一個(gè)進(jìn)程要在每一次輸出通信時(shí)產(chǎn)生一個(gè)新鮮值v；而現(xiàn)在就會(huì)將這次通信變?yōu)橄蛟撨M(jìn)程輸入v，并且要求其與相應(yīng)的NM進(jìn)程同步。

　　為了滿足新鮮值的惟一性和新鮮性，引入的NM進(jìn)程需進(jìn)行下列操作：存儲(chǔ)所有發(fā)送的新鮮值，相同的新鮮值只發(fā)送一次，不發(fā)送屬于攻擊者的新鮮值。顯然這些操作并不滿足PosConjEqT條件。

　　Roscoe沒(méi)有單獨(dú)使用NM進(jìn)程進(jìn)行無(wú)限新鮮值的分發(fā)，而是應(yīng)用數(shù)據(jù)獨(dú)立技術(shù)，在NM進(jìn)程中執(zhí)行Collapse轉(zhuǎn)換，通過(guò)轉(zhuǎn)換從有限集生成無(wú)限新鮮值。

　　Roscoe的數(shù)據(jù)獨(dú)立技術(shù)提供了這樣的理論基礎(chǔ)：若系統(tǒng)的所有成分滿足PosConjEqT′c條件，則大協(xié)議系統(tǒng)中轉(zhuǎn)換前的全部行為(就系統(tǒng)跡而言)可以用經(jīng)過(guò)映射的相應(yīng)的有限系統(tǒng)描述。這一技術(shù)保證了可以在大協(xié)議中應(yīng)用非單映射轉(zhuǎn)換，將問(wèn)題簡(jiǎn)化為相應(yīng)的有限系統(tǒng)。

　　3 數(shù)據(jù)獨(dú)立技術(shù)在CSP協(xié)議模型中的設(shè)計(jì)

　　數(shù)據(jù)獨(dú)立技術(shù)使模型檢測(cè)器的證明更加完整，因?yàn)樗膽?yīng)用使大協(xié)議的建模成為可能。

　　3．1 協(xié)議模型的擴(kuò)展
　　
　　為了解決驗(yàn)證的局限性，需要系統(tǒng)代理能夠在實(shí)際類型保持有限的情況下，調(diào)用無(wú)限的不同的新鮮值。沿用Roscoe的方法，引入Manager進(jìn)程擴(kuò)展CSP協(xié)議模型。與以前的協(xié)議模型相比，該模型引入了Manager進(jìn)程。此進(jìn)程與Intruder進(jìn)程相互配合以實(shí)現(xiàn)新鮮值的循環(huán)利用，因此可視為新鮮值的循環(huán)機(jī)制?？梢哉f(shuō)，該模型是對(duì)Roscoe文獻(xiàn)的一個(gè)擴(kuò)展和細(xì)化，可以證明其滿足PosConjEqT′c條件：

　　(1)進(jìn)程中的數(shù)據(jù)類型隨機(jī)數(shù)Na、Nb和密鑰Kdo均為數(shù)據(jù)獨(dú)立類型。

　　(2)可信代理進(jìn)程為標(biāo)準(zhǔn)類型進(jìn)程，滿足PosConjEqT′c條件。

　　(3)攻擊者進(jìn)程在明確推理系統(tǒng)中建立，并且其初始知識(shí)集不包含對(duì)類型T成員(除了常數(shù)C)的非等價(jià)測(cè)試，滿足P0sConjEqT′c條件。

　　因此該系統(tǒng)中轉(zhuǎn)換前全部行為可以用經(jīng)過(guò)映射的、相應(yīng)的有限系統(tǒng)描述。也正基于此，可以在無(wú)限新鮮值的產(chǎn)生過(guò)程中應(yīng)用非單映射轉(zhuǎn)換，從而將其簡(jiǎn)化為相應(yīng)的有限過(guò)程，以形成完整的形式化描述。

　　3．2 協(xié)議各對(duì)象的描述
　　
　　對(duì)于每一個(gè)新鮮值引入對(duì)應(yīng)的Manager進(jìn)程，取消可信代理分發(fā)新鮮值的能力，只在單次運(yùn)行期間存儲(chǔ)新鮮值，并要求其在完成協(xié)議一次運(yùn)行時(shí)“遺忘”所有存儲(chǔ)的新鮮值。當(dāng)新鮮值v不再被可信參與者所知(存儲(chǔ))時(shí)，稱v被“遺忘”。攻擊者能夠存儲(chǔ)在網(wǎng)絡(luò)中所見(jiàn)的所有新信息。為了能夠產(chǎn)生無(wú)限的新鮮值，可以對(duì)攻擊者存儲(chǔ)的新鮮值應(yīng)用collasphag函數(shù)，從而啟動(dòng)所提出的新鮮值循環(huán)機(jī)制。即當(dāng)新鮮值v在網(wǎng)絡(luò)中被“遺忘”時(shí)可以被循環(huán)再利用。一旦該值被循環(huán)利用，相應(yīng)的Manager進(jìn)程可以在網(wǎng)絡(luò)中再次將其作為新鮮值使用。

　　(1)可信進(jìn)程
　　
　　在擴(kuò)展的CSP協(xié)議模型中，進(jìn)程描述如下：

　　擴(kuò)展后的描述主要有三處變動(dòng)：第一，進(jìn)程被定義為遞歸進(jìn)程，表示Initiator可以執(zhí)行無(wú)限數(shù)量的序列運(yùn)行；而在之前的模型描述中，進(jìn)程在SKIP終止。第二，新鮮Nonce NA不再是參數(shù)，而是來(lái)自集合NonceF(通過(guò)定義，進(jìn)程可以接收該集合中的任意值)；之后將會(huì)介紹Manager進(jìn)程如何終止這些值的產(chǎn)生。第三，添加了close事件表示進(jìn)程重新開(kāi)始執(zhí)行初始狀態(tài)。該事件標(biāo)志著進(jìn)程一次運(yùn)行的結(jié)束，在新鮮值的循環(huán)機(jī)制中發(fā)揮重要作用。