Jean-Francois Raskin (Université Libre de Bruxelles)
Title: Formal Verification of Non-Repudiation Protocols. A Game Approach
Abstract. 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. An optimistic non-repudiation protocol is analyzed using Mocha.