A game-based verification of non-repudiation and fair exchange protocols¹

Article type: Research Article

Authors: Kremer, Steve | Raskin, Jean-François

Affiliations: Département d'Informatique, Faculté des Sciences, Université Libre de Bruxelles, Belgium. E-mail: Steve.Kremer@ulb.ac.be, Jean-Francois.Raskin@ulb.ac.be

Note: [1] Parts of this works have previously been presented in [14].

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.

DOI: 10.3233/JCS-2003-11307

Journal: Journal of Computer Security, vol. 11, no. 3, pp. 399-429, 2003