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

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

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

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