形式化方法在安全協(xié)議驗證領(lǐng)域內(nèi)的應(yīng)用研究.pdf

1、該文中,我們探討了形式化方法在安全協(xié)議驗證領(lǐng)域內(nèi)的相關(guān)應(yīng)用問題.其中,我們工作的重點將集中在Strand空間方法上.首先,我們介紹了安全協(xié)議描述方法發(fā)展的三個階段,由此引出形式化方法應(yīng)用于安全協(xié)議驗證領(lǐng)域內(nèi)的初衷.隨后,我們分三條線索:Dolev-Yao模型及其影響、BAN邏輯與其后續(xù)工作,以及形式化方法的自動化技術(shù),對形式化方法在安全協(xié)議驗證領(lǐng)域內(nèi)的發(fā)展動態(tài)進(jìn)行了全面而客觀的評述.第二,我們概述了該領(lǐng)域內(nèi)三個最具影響力的形式化方法的應(yīng)

2、用過程,它們分別是Dolev-Yao模型、BAN邏輯,與Strand空間.為了進(jìn)一步說明這些方法的實用性,我們還給出了相應(yīng)的實例分析.第三,我們對近來頗受關(guān)注的Strand空間展開了一系列研究.這部分工作基于五個目標(biāo):其一、細(xì)化理想結(jié)構(gòu)的描述方式;基二、形式化表述安全密鑰的概念;其三、揭示安全密鑰與協(xié)議秘密屬性之間的關(guān)系;其四、給出安全密鑰的相關(guān)性質(zhì);其五、提出一個證明安全協(xié)議的新思路.為實現(xiàn)這些目標(biāo),我們引入新的記號以表示理想的內(nèi)部結(jié)

3、構(gòu);利用理想的概念給出了安全密鑰的形式化描述;在特定條件下,通過對比安全密鑰與秘密屬性各自的理想表達(dá),證明了他們之間的等價關(guān)系;借助入侵者密鑰的定義與入侵者行為對應(yīng)的消息序列,證明了安全密鑰特有的性質(zhì);最后,基于以上工作,我們提出一個基于安全密鑰概念的協(xié)議證明思路.第四,我們基于Strand空間提出了一個新的針對安全協(xié)議缺陷的分類法.這個分類法將協(xié)議缺陷分為以下八類:當(dāng)前性缺失缺陷、方向性缺失缺陷、類型缺失缺陷、獨立性缺失缺陷、輪數(shù)標(biāo)識