Wuhan University Journal of Natural Sciences

, Volume 11, Issue 6, pp 1516–1520

# Mechanical proofs about BW multi-party contract signing protocol

Cryptography

## 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.

## Key words

formal verification multi-party contract signing protocol inductive approach model

TP 393. 04

## References

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.
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.
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.
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].http://citeseer.ist.psu.edu/726410.html.Google 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].http://isabelle.in.tum.de/ 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