www.prismmodelchecker.org
[NS02] G. Norman and V. Shmatikov. Analysis of Probabilistic Contract Signing. In A. Abdallah, P. Ryan and S. Schneider (editors), Proc. BCS-FACS Formal Aspects of Security (FASec'02), volume 2629 of Lecture Notes in Computer Science, pages 81-96, Springer. December 2002. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (102 KB)  pdf pdf (275 KB)  bib bib
Notes: Further information and verification results are available from the PRISM web page. The original publication is available at www.springerlink.com.
Abstract. We consider the probabilistic contract signing protocol of Ben-Or, Goldreich, Micali, and Rivest as a case study in formal verification of probabilistic security protocols. Using the probabilistic model checker PRISM, we analyse the probabilistic fairness guarantees the protocol is intended to provide. Our study demonstrates the difficulty of combining fairness with timeliness in the context of probabilistic contract signing. If, as required by timeliness, the judge responds to participants' messages immediately upon receiving them, then there exists a strategy for a misbehaving participant that brings the protocol to an unfair state with arbitrarily high probability, unless unusually strong assumptions are made about the quality of the communication channels between the judge and honest participants. We quantify the tradeoffs involved in the attack strategy, and discuss possible modifications of the protocol that ensure both fairness and timeliness.

Publications