Handling algebraic properties in automatic analysis of security protocols. (English) Zbl 1168.68378

Barkaoui, Kamel (ed.) et al., Theoretical aspects of computing – ICTAC 2006. Third international colloquium, Tunis, Tunisia, November 20–24, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-48815-6/pbk). Lecture Notes in Computer Science 4281, 153-167 (2006).
Summary: In this paper we extend the approximation based theoretical framework in which the security problem – secrecy preservation against an intruder – may be semi-decided through a reachability verification.
We explain how to cope with algebraic properties for an automatic approximation-based analysis of security protocols. We prove that if the initial knowledge of the intruder is a regular tree language, then the security problem may by semi-decided for protocols using cryptographic primitives with algebraic properties. More precisely, an automatically generated approximation function enables us 1) an automatic normalization of transitions, and 2) an automatic completion procedure. The main advantage of our approach is that the approximation function makes it possible to verify security protocols with an arbitrary number of sessions.
The concepts are illustrated on an example of the view-only protocol using a cryptographic primitive with the exclusive or algebraic property.
For the entire collection see [Zbl 1142.68004].


68P25 Data encryption (aspects in computer science)
68Q60 Specification and verification (program logics, model checking, etc.)
94A60 Cryptography


Full Text: DOI Link