论文部分内容阅读
我们在签署 Baum-Waidner 描述的协议的一个多党的合同的确认上报导；Waidner (BW ) 。基于 Paulson 的引入的途径，我们给无穷地包括许多签署者的协议模型；同时签名的合同文章。我们考虑不诚实的签署者的合成攻击；外部入侵者，形式化密码的原语；协议算术包括攻击模型，显示出对关键分发的正式描述，；证明签名钥匙秘密定理；用交互定理的 BW 协议的公平性质定理，证明器 Isabelle/HOL。