數據獨立技術在CSP協議模型中的設計
加入技術交流群
協議模型中的代理進程是標準類型進程且易于進行滿足PosConjEqT′c條件的特性檢測。但Intruder進程可以依靠推理系統指定產生或破壞信息的規則，這一特性決定了其更為復雜。
如果推理系統滿足這樣的條件，即對于類型間的任意函數φ：T1→T2，只要(X,f)是系統產生的適用于類型T1推論，則(φ(X)，φ(f))就是適用于T2的推論，進而稱該推理系統與這些類型參數T明確相關。其中要求推理的產生在T上對稱(也就是平等對待T的所有成員)并且對出現在推理左邊的T成員不再具有不等的要求。本文引用地址：http://www.104case.com/article/155601.htm
從上述定義可以確定這樣的性質：如果在明確推理系統中建立攻擊者，并且攻擊者的初始知識集不包含對于類型T成員(除了常數C)的非等價測試，那么該進程滿足PosConjEqT′c條件(并且因此，整個協議模型滿足網絡其他部分的條件)。
可以看出系統成分是否滿足上述性質對研究至關重要。只有滿足這些條件才能夠在協議分析的CSP模型中構造更為復雜的事件。
Roscoe在文獻中引入了NM進程，負責產生系統所需的無眼新鮮值。那么在以前運行中，一個進程要在每一次輸出通信時產生一個新鮮值v；而現在就會將這次通信變為向該進程輸入v，并且要求其與相應的NM進程同步。
為了滿足新鮮值的惟一性和新鮮性，引入的NM進程需進行下列操作：存儲所有發送的新鮮值，相同的新鮮值只發送一次，不發送屬于攻擊者的新鮮值。顯然這些操作并不滿足PosConjEqT條件。
Roscoe沒有單獨使用NM進程進行無限新鮮值的分發，而是應用數據獨立技術，在NM進程中執行Collapse轉換，通過轉換從有限集生成無限新鮮值。
Roscoe的數據獨立技術提供了這樣的理論基礎：若系統的所有成分滿足PosConjEqT′c條件，則大協議系統中轉換前的全部行為(就系統跡而言)可以用經過映射的相應的有限系統描述。這一技術保證了可以在大協議中應用非單映射轉換，將問題簡化為相應的有限系統。
3 數據獨立技術在CSP協議模型中的設計
數據獨立技術使模型檢測器的證明更加完整，因為它的應用使大協議的建模成為可能。
3．1 協議模型的擴展
為了解決驗證的局限性，需要系統代理能夠在實際類型保持有限的情況下，調用無限的不同的新鮮值。沿用Roscoe的方法，引入Manager進程擴展CSP協議模型。與以前的協議模型相比，該模型引入了Manager進程。此進程與Intruder進程相互配合以實現新鮮值的循環利用，因此可視為新鮮值的循環機制。可以說，該模型是對Roscoe文獻的一個擴展和細化，可以證明其滿足PosConjEqT′c條件：
(1)進程中的數據類型隨機數Na、Nb和密鑰Kdo均為數據獨立類型。
(2)可信代理進程為標準類型進程，滿足PosConjEqT′c條件。
(3)攻擊者進程在明確推理系統中建立，并且其初始知識集不包含對類型T成員(除了常數C)的非等價測試，滿足P0sConjEqT′c條件。
因此該系統中轉換前全部行為可以用經過映射的、相應的有限系統描述。也正基于此，可以在無限新鮮值的產生過程中應用非單映射轉換，從而將其簡化為相應的有限過程，以形成完整的形式化描述。
3．2 協議各對象的描述
對于每一個新鮮值引入對應的Manager進程，取消可信代理分發新鮮值的能力，只在單次運行期間存儲新鮮值，并要求其在完成協議一次運行時“遺忘”所有存儲的新鮮值。當新鮮值v不再被可信參與者所知(存儲)時，稱v被“遺忘”。攻擊者能夠存儲在網絡中所見的所有新信息。為了能夠產生無限的新鮮值，可以對攻擊者存儲的新鮮值應用collasphag函數，從而啟動所提出的新鮮值循環機制。即當新鮮值v在網絡中被“遺忘”時可以被循環再利用。一旦該值被循環利用，相應的Manager進程可以在網絡中再次將其作為新鮮值使用。
(1)可信進程
在擴展的CSP協議模型中，進程描述如下：
擴展后的描述主要有三處變動：第一，進程被定義為遞歸進程，表示Initiator可以執行無限數量的序列運行；而在之前的模型描述中，進程在SKIP終止。第二，新鮮Nonce NA不再是參數，而是來自集合NonceF(通過定義，進程可以接收該集合中的任意值)；之后將會介紹Manager進程如何終止這些值的產生。第三，添加了close事件表示進程重新開始執行初始狀態。該事件標志著進程一次運行的結束，在新鮮值的循環機制中發揮重要作用。
評論