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. Journal of Computer Security, 11(3):399–429, IOS Press, 2003.

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

@article{KremerRaskin2003,
  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}.},
  author =        {Kremer, Steve and Raskin, Jean-Fran{\c{c}}ois},
  journal =       {Journal of Computer Security},
  number =        {3},
  pages =         {399-429},
  publisher =     {{IOS} Press},
  title =         {A Game-Based Verification of Non-Repudiation and Fair
                   Exchange Protocols},
  volume =        {11},
  year =          {2003},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Kremer-gameNRextended.ps},
}