Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
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.
Garay J, MacKenzie P. Abuse-Free Multi-Party Contract Signing [J].Lecture Notes in Computer Science, 1999,1693:151–165.
Garay J A, Jakobsson M, MacKenzie P D. Abuse-Free Optimistic Contract Signing [J].Lecture Notes in Computer Science, 1999,1666:449–446.
Shmatikov V, Mitchell J. Analysis of Abuse-Free Contract Signing [J].Lecture Notes in Computer Science, 2000,1962:174–191.
Shmatikov V, Mitchell J. Finite-State Analysis of Two Contract Signing Protocols [J].Theoretical Computer Science, 2002,283(2):419–450.
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.
Chadha R, Kremer S, Scedrov A. Formal Analysis of Multi-Party Contract Signing [DB/OL]. [2005-09-01].http://citeseer.ist.psu.edu/726410.html.
Paulson L C. The Inductive Approach to Verifying Cryptographic Protocols [J].Computer Security, 1988,6:85–128.
Paulson L C. A Proof Assistant for Higher-Order Logic [DB/OL]. [2005-09-01].http://isabelle.in.tum.de/
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.
Author information
Authors and Affiliations
Corresponding author
Additional information
Foundation item: Supported by the National Natural Science Foundation of China (60373068).
Biography: ZHANG Ningrong (1972-) female, Ph. D. candidate, research direction: information security and electronic commerce.
Rights and permissions
About this article
Cite this article
Ningrong, Z., Xingyuan, Z. & Yuanyuan, W. Mechanical proofs about BW multi-party contract signing protocol. Wuhan Univ. J. Nat. Sci. 11, 1516–1520 (2006). https://doi.org/10.1007/BF02831810
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF02831810