Mechanical proofs about BW multi-party contract signing protocol
- 30 Downloads
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 wordsformal verification multi-party contract signing protocol inductive approach model
CLC numberTP 393. 04
Unable to display preview. Download preview PDF.
- Garay J, MacKenzie P. Abuse-Free Multi-Party Contract Signing [J].Lecture Notes in Computer Science, 1999,1693:151–165.Google Scholar
- Shmatikov V, Mitchell J. Analysis of Abuse-Free Contract Signing [J].Lecture Notes in Computer Science, 2000,1962:174–191.Google Scholar
- 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
- 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.Google Scholar
- Paulson L C. The Inductive Approach to Verifying Cryptographic Protocols [J].Computer Security, 1988,6:85–128.Google Scholar
- Paulson L C. A Proof Assistant for Higher-Order Logic [DB/OL]. [2005-09-01].http://isabelle.in.tum.de/ Google Scholar
- 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