Istituto di Scienza e Tecnologie dell'Informazione     
Ter Beek M. H., Lenzini G., Petrocchi M. A team automaton scenario for the analysis of security properties in communication protocols. In: Journal of Automata, Languages and Combinatorics, vol. 11 (4) pp. 345 - 374. Otto-von-Guericke-Universitat Magdeburg, 2006.
Formal methods are a popular means to specify and verify security properties of a variety of communication protocols. In this article we take a step towards the use of team automata for the analysis of security aspects in such protocols. To this aim, we define an insecure communication scenario for team automata that is general enough to encompass various communication protocols. We then reformulate the Generalized Non-Deducibility on Compositions schema - originally introduced in the context of process algebrae - in terms of team automata. Based on the resulting team automata framework, we subsequently develop two analysis strategies that can be used to verify security properties of communication protocols. Indeed, the paper concludes with two case studies in which we show how our framework can be used to prove integrity and secrecy in two different settings: We show how integrity is guaranteed in a team automaton model of a particular instance of the Efficient Multi-chained Stream Signature protocol, a communication protocol for signing digital streams that provides some robustness against packet loss, and we show how secrecy is preserved when a member of a multicast group leaves the group in a particular run of the complementary variable approach to the N-Root/Leaf pairwise keys protocol.
URL: http://fmt.isti.cnr.it/~mtbeek/jalc.pdf
Subject Team automata
Security analysis
Security properties
Communication protocols
D.2.4 Software/Program Verification. Formal methods
D.4.6 Security and Protection. Verification
F.1.1 Models of Computation. Automata

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional