安全協(xié)議分析的形式化理論與方法——基于定理證明的安全協(xié)議建模研究.pdf

1、安全的密碼協(xié)議是網(wǎng)絡(luò)通信和應(yīng)用必不可少的組件之一，是構(gòu)筑信息安全體系的基礎(chǔ)。設(shè)計(jì)安全和有效的密碼協(xié)議是協(xié)議工程領(lǐng)域中的主要研究?jī)?nèi)容。在設(shè)計(jì)、描述(建模)、驗(yàn)證、性能分析、實(shí)現(xiàn)、測(cè)試和維護(hù)等協(xié)議工程的各個(gè)環(huán)節(jié)中，協(xié)議驗(yàn)證是最為關(guān)鍵的一個(gè)環(huán)節(jié)。協(xié)議分析和協(xié)議綜合是實(shí)現(xiàn)協(xié)議驗(yàn)證的兩種有效途徑，前者更為有效和實(shí)用。 自上個(gè)世紀(jì)七十年代末以來(lái)，人們提出多種安全協(xié)議分析的形式化理論，包括Dolev-Yao模型、模態(tài)邏輯、Paulson歸納法

2、、串空間模型以及Spi演算理論等，并從這些理論中歸納出基于模態(tài)邏輯推理、基于模型狀態(tài)檢驗(yàn)、基于定理證明和基于類型檢測(cè)等安全目標(biāo)驗(yàn)證方法。前兩類方法只能推理密碼協(xié)議的不安全性，不能給出其安全目標(biāo)的可信證明，而后一類方法又不具有完備性，唯有基于定理證明的安全目標(biāo)驗(yàn)證方法試圖給出密碼協(xié)議的安全性證明。 本文在基于定理證明的安全協(xié)議形式化建模方面系統(tǒng)地研究了安全協(xié)議的消息語(yǔ)句空間和消息事件空間的性質(zhì)、主體進(jìn)程表示理論以及安全目標(biāo)的分類、

3、形式化描述和安全協(xié)議的可驗(yàn)證性等問(wèn)題，主要工作和貢獻(xiàn)如下： 1.研究消息語(yǔ)句空間性質(zhì)，提出用于消息語(yǔ)句結(jié)構(gòu)定性和定量分析的理論與方法。消息語(yǔ)句空間及其語(yǔ)句運(yùn)算構(gòu)成消息代數(shù)。其語(yǔ)句運(yùn)算包括f-語(yǔ)句運(yùn)算、求逆密鑰運(yùn)算以及語(yǔ)句的加密和連接運(yùn)算。這些運(yùn)算可以完備地生成現(xiàn)有安全協(xié)議運(yùn)行中主體角色(包括攻擊者)的各種消息語(yǔ)句。消息代數(shù)中的代數(shù)運(yùn)算規(guī)則和子句關(guān)系是定量和定性語(yǔ)句結(jié)構(gòu)分析的理論工具。 2.研究消息事件空間性質(zhì)，提出用于消

4、息事件動(dòng)態(tài)分析的消息交換關(guān)系理論。由利用前驅(qū)關(guān)系排序主體角色消息事件集中的消息事件得到的消息事件序列為進(jìn)程順序合成運(yùn)算提供了語(yǔ)義模型。通過(guò)定義可達(dá)路徑對(duì)特征消息語(yǔ)句單元在消息交換中的遷移狀況的刻畫，給出組合(并發(fā)運(yùn)行)協(xié)議中的主協(xié)議(觀察對(duì)象)保持其獨(dú)立性的判定定理。 3.以已有的進(jìn)程代數(shù)(Spi演算)理論為基礎(chǔ)，研究了安全協(xié)議并發(fā)運(yùn)行系統(tǒng)主體進(jìn)程的表示理論，提出一種進(jìn)程描述語(yǔ)言，將主體角色消息事件序列的生成、主體角色消息事件序

5、列之間的通信以及主體角色消息事件之間路徑的事件序列集合存在M-劃分的情形描述為主體進(jìn)程順序演算、并行演算以及選擇演算的語(yǔ)義模型。在此基礎(chǔ)上，給出主體進(jìn)程演算的算法及其互模擬刻畫。 4.提出一種用于并發(fā)運(yùn)行安全協(xié)議形式化描述的事件圖模型。給出消息事件之間的通信關(guān)系和前驅(qū)關(guān)系以及消息語(yǔ)句的新鮮性約束刻畫。建立圖元，并將其作為事件圖的生成單元。通過(guò)定義用于描述消息事件之間、圖元之間和消息事件與圖元之間的運(yùn)算算子，給出事件圖的生成算法。

6、以圖元的互模擬來(lái)度量事件圖的互模擬等價(jià)關(guān)系，并給出用于消除事件圖冗余的規(guī)則。事件圖模型可以看作是對(duì)現(xiàn)有的Spi演算理論和串空間理論的融合和擴(kuò)展。 5.基于全局最小K-理想誠(chéng)實(shí)性判定理論，提出一種安全目標(biāo)驗(yàn)證方法。以f-語(yǔ)句運(yùn)算、求逆密鑰運(yùn)算以及語(yǔ)句的加密和連接運(yùn)算為基礎(chǔ)，定義一種稱為最小K-理想的不變集。給出不變集誠(chéng)實(shí)性判定定理及其證明，并提出誠(chéng)實(shí)性判定條件的可滿足性定理和最小K-理想的構(gòu)造算法。該結(jié)果擴(kuò)展了現(xiàn)有的串空間理論。