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.
CITATION STYLE
Kremer, S., & Raskin, J. F. (2001). A game-based verification of non-repudiation and fair exchange protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2154, pp. 551–565). Springer Verlag. https://doi.org/10.1007/3-540-44685-0_37
Mendeley helps you to discover research relevant for your work.