Analysis of Probabilistic Contract Signing

Gethin Norman, V Shmatikov, A Abdallah, P Ryan, S Schneider

Research output: Contribution to journalArticlepeer-review

15 Citations (Scopus)


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.
Original languageEnglish
Pages (from-to)81-96
Number of pages16
JournalLecture Notes in Computer Science
Publication statusPublished - 1 Jan 2003
EventBCS-FACS Formal Aspects of Security -
Duration: 1 Jan 2003 → …


Dive into the research topics of 'Analysis of Probabilistic Contract Signing'. Together they form a unique fingerprint.

Cite this