Steve Kremer: Formal Analysis of Multi-Party Contract Signing

Formal Analysis of Multi-Party Contract Signing

Rohit Chadha, Steve Kremer, and Andre Scedrov. Formal Analysis of Multi-Party Contract Signing. In Preliminary Proceedings of the 4th IFIP WG1.7 Workshop on Issues in the Theory of Security (WITS'04), pp. 153–163, Barcelona, Spain, April 2004.

Download

[PS]

Abstract

We analyze the multi-party contract-signing protocols of Garay and MacKenzie (GM) and of Baum and Waidner (BW). We use a finite-state tool, Mocha, which allows specification of protocol properties in a branching-time temporal logic with game semantics. While our analysis does not reveal any errors in the BW protocol, in the GM protocol we discover serious problems with fairness for four signers and an oversight regarding abuse-freeness for three signers. We propose a complete revision of the GM subprotocols in order to restore fairness.

BibTeX

@inproceedings{ChadhaKremerScedrov2004,
  abstract =      {We analyze the multi-party contract-signing protocols
                   of Garay and MacKenzie (GM) and of Baum and Waidner
                   (BW). We use a finite-state tool, {\scshape Mocha},
                   which allows specification of protocol properties in
                   a branching-time temporal logic with game semantics.
                   While our analysis does not reveal any errors in the
                   BW protocol, in the GM protocol we discover serious
                   problems with fairness for four signers and an
                   oversight regarding abuse-freeness for three signers.
                   We propose a complete revision of the GM subprotocols
                   in order to restore fairness.},
  address =       {Barcelona, Spain},
  author =        {Chadha, Rohit and Kremer, Steve and Scedrov, Andre},
  booktitle =     {{P}reliminary {P}roceedings of the 4th {IFIP} {WG1.7}
                   {W}orkshop on {I}ssues in the {T}heory of {S}ecurity
                   ({WITS}'04)},
  editor =        {Ryan, Peter},
  month =         apr,
  pages =         {153-163},
  title =         {Formal Analysis of Multi-Party Contract Signing},
  year =          {2004},
  acronym =       {{WITS}'04},
  nmonth =        {4},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Kremer-wits04.ps},
}