Steve Kremer: Game Analysis of Abuse-Free Contract Signing

Game Analysis of Abuse-Free Contract Signing

Steve Kremer and Jean-François Raskin. Game Analysis of Abuse-Free Contract Signing. In Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW'02), pp. 206–220, IEEE Computer Society Press, Cape Breton, Nova Scotia, Canada, June 2002.

Download

[PS]

Abstract

In this paper we report on the verification of two contract signing protocols. Our verification method is based on the idea of modeling those protocols as games, and reasoning about their properties as strategies for players. We use the formal model of alternating transition systems to represent the protocols and alternating-time temporal logic to specify properties. The paper focuses on the verification of abuse-freeness, relates this property to the balance property, previously studied using two other formalisms, shows some ambugities in the definition of abuse-freeness and proposes a new, stronger definition. Formal methods are not only useful here to verify automatically the protocols but also to better understand their requirements (balance and abuse-freeness are quite complicated and subtle properties).

BibTeX

@inproceedings{KremerRaskin2002,
  abstract =      {In this paper we report on the verification of two
                   contract signing protocols. Our verification method
                   is based on the idea of modeling those protocols as
                   games, and reasoning about their properties as
                   strategies for players. We use the formal model of
                   alternating transition systems to represent the
                   protocols and alternating-time temporal logic to
                   specify properties. The paper focuses on the
                   verification of abuse-freeness, relates this property
                   to the balance property, previously studied using two
                   other formalisms, shows some ambugities in the
                   definition of abuse-freeness and proposes a new,
                   stronger definition. Formal methods are not only
                   useful here to verify automatically the protocols but
                   also to better understand their requirements (balance
                   and abuse-freeness are quite complicated and subtle
                   properties).},
  address =       {Cape Breton, Nova Scotia, Canada},
  author =        {Kremer, Steve and Raskin, Jean-Fran{\c{c}}ois},
  booktitle =     {{P}roceedings of the 15th {IEEE} {C}omputer
                   {S}ecurity {F}oundations {W}orkshop ({CSFW}'02)},
  month =         jun,
  pages =         {206-220},
  publisher =     {{IEEE} Computer Society Press},
  title =         {Game Analysis of Abuse-Free Contract Signing},
  year =          {2002},
  acronym =       {{CSFW}'02},
  nmonth =        {6},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Kremer-csfw15.ps},
}