基于概率進程演算的安全協(xié)議自動化分析技術(shù)研究.pdf

1、安全協(xié)議的設(shè)計與驗證是信息安全領(lǐng)域中非常重要的內(nèi)容。形式化方法是安全協(xié)議驗證的一個強有力的工具。借助自動化工具，應(yīng)用形式化方法來分析安全協(xié)議，是當(dāng)今重要的研究課題。形式化方法分為：符號方法和計算方法，符號方法把密碼原語看作完美的黑盒，易于獲得自動化工具的支持，但是不能夠建立密碼學(xué)可靠性；計算方法基于計算復(fù)雜性和概率理論，可以建立密碼學(xué)可靠的證明，但是不易獲得自動化工具的支持。
　　 可否認(rèn)認(rèn)證協(xié)議是安全協(xié)議中的一類重要的協(xié)議，廣

2、泛應(yīng)用于電子政務(wù)中。傳統(tǒng)的對可否認(rèn)性的證明是基于符號方法的，且手工的，容易產(chǎn)生錯誤，沒有建立密碼學(xué)可靠性。本文引入一種基于計算模型的概率進程演算：Blanchet 演算，對可否認(rèn)認(rèn)證協(xié)議中的可否認(rèn)性進行了分析與證明。主要工作如下：
　　 (1)對安全協(xié)議的形式化涉及到的技術(shù)做了一個比較完整的概述。重點介紹了安全協(xié)議的相關(guān)理論和分析技術(shù)。
　　 (2) 首先對計算模型，Blanchet 演算和CryptoVerif 工具進

3、行了詳細(xì)的介紹，包括語法和非形式化語義、類型系統(tǒng)、形式化語義、觀察等價，Game 轉(zhuǎn)換，并給出簡單的示例。然后基于Blanchet 演算，提出一個支持CryptoVerif的可否認(rèn)性證明模型。采用此模型，對Fan等人提出的可否認(rèn)認(rèn)證協(xié)議的可否認(rèn)性進行了分析和證明。
　　 (3)基于橢圓曲線的離散對數(shù)困難問題，提出一個非交互式可否認(rèn)認(rèn)證協(xié)議。并且基于提出的可否認(rèn)性證明模型，應(yīng)用 Blanchet 概率演算和CryptoVerif