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

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

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