Fiche du document
25 septembre 2013
- handle: 10670/1.lbyx3s
- hal: hal-01496073
- doi: 10.1007/978-3-642-40925-7_25
Ce document est lié à :
info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-40925-7_25
http://creativecommons.org/licenses/by/ , info:eu-repo/semantics/OpenAccess
Sujets proches
Natural science Sciences Science of science Pattern ModelCiter ce document
Mirosław Kurkowski et al., « Using Backward Induction Techniques in (Timed) Security Protocols Verification », HAL-SHS : sciences de l'information, de la communication et des bibliothèques, ID : 10.1007/978-3-642-40925-7_25
Métriques
Partage / Export
Résumé
This paper shows a new way of automatic verification of properties of untimed and timed security protocols. To do this we use a modified version of previously introduced formal model based on a network of synchronized (timed) automata that expreses behaviour and distributed knowledge of users during protocol executions. In our new approach we will use the backward induction method for searching of a tree of all real executions of an investigated protocol. Our approach uses additionally the boolean encoding of constructed structures and SAT solvers for searching answers to the questions about investigated properties which are expressed as reachability or unreachability of undesired states in a considered model. We exemplify all our notions and formalisms on the well known NSPK, and show experimental results for checking authentication and security properties of a few untimed and timed protocols.