引入局部可操作函數(shù)的實例空間安全協(xié)議分析法.pdf

1、安全協(xié)議的驗證是網(wǎng)絡安全研究中的熱點和難點，本文把局部可操作函數(shù)引入到實例空間協(xié)議分析方法中，簡化了協(xié)議的描述和分析，增強了實例空間方法的可擴展性，并用新的理論框架分析了JFKi和JFKr協(xié)議核心部分的兩個安全性質(zhì)。JFK協(xié)議是新近提出的以代替IKE協(xié)議為目標的密鑰交換協(xié)議，它提供很多安全服務，分析它的安全性具有很高的研究和應用價值。本文證明了JFKi協(xié)議核心部分滿足相互認證性和協(xié)商密鑰秘密性，而JFKr協(xié)議核心部分只保證協(xié)商密鑰的秘密

2、性。 本文首先提出一個引進局部可操作函數(shù)的消息交換模型作為協(xié)議的執(zhí)行模型。局部可操作函數(shù)用于表示主體對消息的操作，包括聯(lián)接、分解、加密、解密、簽名、Hash計算等，代表了主體的能力。引入局部可操作函數(shù)后，消息交換模型的分析函數(shù)如Poss、Sees等的定義更為簡單，而更重要的是，它們的描述能力更強。另外，本文還證明了擴展的消息交換模型的很多定理。接著本文介紹了引入局部可操作函數(shù)項的與消息交換模型相對應的協(xié)議描述模型，并重新定義了它

3、們之間的關聯(lián)函數(shù)——實例函數(shù)。在實例函數(shù)的基礎上本文定義了實例空間并證明了很多關于實例空間原子命題的性質(zhì)，其中有不少是引入局部可操作函數(shù)后增加或修改的。這些性質(zhì)和消息交換模型中的定理都是我們分析協(xié)議安全性的關鍵。其中最為重要的是(n，1)-SecrecyProperties，本文利用局部可操作函數(shù)的概念重新定義了消息泄漏和獲取函數(shù)，并重新證明了(n，1)-SecrecyProperties。最后本文利用這個擴展了的實例空間協(xié)議分析方法結