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

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

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