Steve Kremer: A Game-Based Verification of Non-Repudiation and Fair Exchange Protocols

A Game-Based Verification of Non-Repudiation and Fair Exchange Protocols

Steve Kremer and Jean-François Raskin. A Game-Based Verification of Non-Repudiation and Fair Exchange Protocols. In Proceedings of the 12th International Conference on Concurrency Theory (CONCUR'01), pp. 551–565, Lecture Notes in Computer Science 2154, Springer, Aalborg, Denmark, August 2001.

Download

[PS]

Abstract

In this paper, we report on a recent work for the verification of non-repudiation protocols. We propose a verification method based on the idea that non-repudiation protocols are best modeled as games. To formalize this idea, we use alternating transition systems, a game based model, to model protocols and alternating temporal logic, a game based logic, to express requirements that the protocols must ensure. This method is automated by using the model-checker Mocha, a model-checker that supports the alternating transition systems and the alternating temporal logic. Several optimistic protocols are analyzed using Mocha.

BibTeX

@inproceedings{KremerRaskin2001,
  abstract =      {In this paper, we report on a recent work for the
                   verification of non-repudiation protocols. We propose
                   a verification method based on the idea that
                   non-repudiation protocols are best modeled as games.
                   To formalize this idea, we use alternating transition
                   systems, a game based model, to model protocols and
                   alternating temporal logic, a game based logic, to
                   express requirements that the protocols must ensure.
                   This method is automated by using the model-checker
                   {\scshape Mocha}, a model-checker that supports the
                   alternating transition systems and the alternating
                   temporal logic. Several optimistic protocols are
                   analyzed using {\scshape Mocha}.},
  address =       {Aalborg, Denmark},
  author =        {Kremer, Steve and Raskin, Jean-Fran{\c{c}}ois},
  booktitle =     {{P}roceedings of the 12th {I}nternational
                   {C}onference on {C}oncurrency {T}heory ({CONCUR}'01)},
  editor =        {Larsen, Kim G. and Nielsen, Modens},
  month =         aug,
  pages =         {551-565},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {A Game-Based Verification of Non-Repudiation and Fair
                   Exchange Protocols},
  volume =        {2154},
  year =          {2001},
  acronym =       {{CONCUR}'01},
  nmonth =        {8},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Kremer-concur01.ps},
}