Sciweavers

Share
JALC
2006

A Team Automaton Scenario for the Analysis of Security Properties of Communication Protocols

9 years 11 months ago
A Team Automaton Scenario for the Analysis of Security Properties of Communication Protocols
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 Sig...
Maurice H. ter Beek, Gabriele Lenzini, Marinella P
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JALC
Authors Maurice H. ter Beek, Gabriele Lenzini, Marinella Petrocchi
Comments (0)
books