Wuhan University Journal of Natural Sciences

, Volume 11, Issue 6, pp 1516–1520 | Cite as

Mechanical proofs about BW multi-party contract signing protocol

  • Zhang Ningrong
  • Zhang Xingyuan
  • Wang Yuanyuan


We report on the verification of a multi-party contract signing protocol described by Baum-Waidner and Waidner (BW). Based on Paulson's inductive approach, we give the protocol model that includes infinitely many signatories and contract texts signing simultaneously. We consider composite attacks of the dishonest signatory and the external intruder, formalize cryptographic primitives and protocol arithmetic including attack model, show formal description of key distribution, and prove signature key secrecy theorems and fairness property theorems of the BW protocol using the interactive theorem, prover Isabelle/HOL.

Key words

formal verification multi-party contract signing protocol inductive approach model 

CLC number

TP 393. 04 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Baum-Waidner B, Waidner M. Round-Optimal and Abuse Free Optimistic Multi-Party Contract Signing [J].Lecture Notes in Computer Science, 2000,1853:524–535.MathSciNetCrossRefGoogle Scholar
  2. [2]
    Garay J, MacKenzie P. Abuse-Free Multi-Party Contract Signing [J].Lecture Notes in Computer Science, 1999,1693:151–165.Google Scholar
  3. [3]
    Garay J A, Jakobsson M, MacKenzie P D. Abuse-Free Optimistic Contract Signing [J].Lecture Notes in Computer Science, 1999,1666:449–446.MathSciNetGoogle Scholar
  4. [4]
    Shmatikov V, Mitchell J. Analysis of Abuse-Free Contract Signing [J].Lecture Notes in Computer Science, 2000,1962:174–191.Google Scholar
  5. [5]
    Shmatikov V, Mitchell J. Finite-State Analysis of Two Contract Signing Protocols [J].Theoretical Computer Science, 2002,283(2):419–450.MATHCrossRefMathSciNetGoogle Scholar
  6. [6]
    Chadha R, Kanovich M, Scedrov A. Inductive Methods and Contract-Signing Protocols [C]//8th ACM Conference on Computer and Communications Security. New York: IEEE Computer Society Press, 2002:176–185.Google Scholar
  7. [7]
    Chadha R, Kremer S, Scedrov A. Formal Analysis of Multi-Party Contract Signing [DB/OL]. [2005-09-01]. Scholar
  8. [8]
    Paulson L C. The Inductive Approach to Verifying Cryptographic Protocols [J].Computer Security, 1988,6:85–128.Google Scholar
  9. [9]
    Paulson L C. A Proof Assistant for Higher-Order Logic [DB/OL]. [2005-09-01]. Google Scholar
  10. [10]
    Zhang Xingyuan, Yang Huabing, Wang Yuanyuan. Liveness Reasoning for Inductive Protocol Verification [C]. //The ‘Emerging Trend’ of TPHOLs 2005. Oxford: Oxford University Press, 2005:221–235.Google Scholar

Copyright information

© Springer 2006

Authors and Affiliations

  1. 1.Institute of Command AutomationPLA University of Science and TechnologyNanjing, JiangsuChina

Personalised recommendations