基于Spi演算的安全協(xié)議形式化分析.pdf

1、安全的密碼協(xié)議是構(gòu)筑信息安全體系的基礎(chǔ)，是網(wǎng)絡(luò)通信和應(yīng)用必不可少的組件之一。不過，已有的安全協(xié)議往往被證實(shí)并不如它們的設(shè)計(jì)所期望的那樣安全。由于安全協(xié)議具有安全目標(biāo)定義的微妙性，運(yùn)行環(huán)境的復(fù)雜性，攻擊者能力的不確定性和協(xié)議執(zhí)行的高并發(fā)性，驗(yàn)證安全協(xié)議具有很多難點(diǎn)。因此我們必須借助形式化的方法對安全協(xié)議進(jìn)行安全分析和驗(yàn)證。自上個世紀(jì)七十年代末以來，人們提出了多種安全協(xié)議分析的形式化理論，主要有基于知識與信念推理的模態(tài)邏輯方法，基于定理證明

2、的方法和基于進(jìn)程演算的方法三種。其中，基于進(jìn)程演算的方法對于協(xié)議的描述十分接近協(xié)議的本身含義，可以很精確地刻畫協(xié)議的整個交互過程。Spi演算是在經(jīng)典進(jìn)程演算理論的基礎(chǔ)上，為刻畫安全協(xié)議而專門提出來的一種演算。Spi演算擴(kuò)展了基本的密碼操作原語，適合多輪并發(fā)條件下安全協(xié)議的分析驗(yàn)證。本文對基于進(jìn)程演算的驗(yàn)證方法作了一定的研究，以Spi演算為核心，依托互模擬等價技術(shù)對安全協(xié)議進(jìn)行分析。論文主要內(nèi)容包括：1)總結(jié)安全協(xié)議驗(yàn)證的幾種形式化方法，

3、論述其主要概念以及驗(yàn)證實(shí)現(xiàn)的基本思想，深入探討基于進(jìn)程演算的協(xié)議分析方法。并以Spi演算為基礎(chǔ)，以互模擬等價關(guān)系理論為依托，對協(xié)議驗(yàn)證分析的整個過程進(jìn)行梳理。2)對如何利用pi演算對安全協(xié)議進(jìn)行初步描述進(jìn)行了表述，在這個過程中，討論了引入Spi演算的必要性。對強(qiáng)互模擬等價關(guān)系的語義進(jìn)行闡述和分析，并指出其在協(xié)議驗(yàn)證中過于嚴(yán)格，進(jìn)一步，引入測試等價刻畫協(xié)議的安全屬性。3)為了簡化協(xié)議的驗(yàn)證過程，本文介紹了框架互模擬關(guān)系和barbed同余關(guān)