密码协议形式化分析方法分为符号方法与计算方法两类。符号方法假设密码算法是完美的,但没有论证该假设的正确性。计算方法考虑了攻击者对密码算法的分析能力,接近协议的实际运行。目前,人们致力于在计算方法框架下论证完美假设的正确性,以建立符号方法的计算可靠性。Micciancio-Warinschi模型是该领域的经典模型,它给出了在主动攻击下建立符号方法计算可靠性的一般方法,但仅针对公钥加密原语和协议的认证性进行研究,且没有体现完美算法的随机性,不能分析包含{{m}_k}_k,类型消息的协议。鉴于此,本文给出了具有计算可靠性的扩展Micciancio-Warinschi符号方法,以扩展Micciancio-Warinschi模型的应用范围。本文所做的工作主要包括以下几点:1.基于Micciancio-Warinschi方法提出了扩展Micciancio-Warinschi方法,在该扩展方法内建立了使用数字签名、对称加密以及公钥加密等密码原语的扩展标记符号模型与扩展计算模型,并论证了扩展标记符号模型的计算可靠性。这是本文工作的重点与难点。2.用扩展Micciancio-Warinschi方法对NS公钥协议和NSL公钥协议进行了手工推导,得到的结果与理论一致,证明了扩展Micciancio-Warinschi方法的正确性。3.为使扩展标记符号模型便于机器分析与处理,给出了扩展标记符号模型的随机变换,并证明了随机变换的正确性。4.给出了扩展标记符号模型计算可靠性验证的原理、结构及工作流程,并利用现有验证工具实现了该模型的计算可靠性验证。