安全协议的设计与验证是信息安全领域中非常重要的内容。形式化方法是安全协议验证的一个强有力的工具。借助自动化工具,应用形式化方法来分析安全协议,是当今重要的研究课题。形式化方法分为:符号方法和计算方法,符号方法把密码原语看作完美的黑盒,易于获得自动化工具的支持,但是不能够建立密码学可靠性;计算方法基于计算复杂性和概率理论,可以建立密码学可靠的证明,但是不易获得自动化工具的支持。可否认认证协议是安全协议中的一类重要的协议,广泛应用于电子政务中。传统的对可否认性的证明是基于符号方法的,且手工的,容易产生错误,没有建立密码学可靠性。本文引入一种基于计算模型的概率进程演算:Blanchet演算,对可否认认证协议中的可否认性进行了分析与证明。主要工作如下:(1)对安全协议的形式化涉及到的技术做了一个比较完整的概述。重点介绍了安全协议的相关理论和分析技术。(2)首先对计算模型,Blanchet演算和CryptoVerif工具进行了详细的介绍,包括语法和非形式化语义、类型系统、形式化语义、观察等价,Game转换,并给出简单的示例。然后基于Blanchet演算,提出一个支持CryptoVerif的可否认性证明模型。采用此模型,对Fan等人提出的可否认认证协议的可否认性进行了分析和证明。(3)基于椭圆曲线的离散对数困难问题,提出一个非交互式可否认认证协议。并且基于提出的可否认性证明模型,应用Blanchet概率演算和CryptoVerif工具对其可否认性进行了分析和验证。