Sciweavers

Share
CADE
2008
Springer

Proving Group Protocols Secure Against Eavesdroppers

9 years 2 months ago
Proving Group Protocols Secure Against Eavesdroppers
Security protocols are small programs designed to ensure properties such as secrecy of messages or authentication of parties in a hostile environment. In this paper we investigate automated verification of a particular type of security protocols, called group protocols, in the presence of an eavesdropper, i.e., a passive attacker. The specificity of group protocols is that the number of participants is not bounded. Our approach consists in representing an infinite set of messages exchanged during an unbounded number of sessions, one session for each possible number of participants, as well as the infinite set of associated secrets. We use so-called visibly tree automata with memory and structural constraints (introduced recently by Comon-Lundh et al.) to represent over-approximations of these two sets. We identify restrictions on the specification of protocols which allow us to reduce the attacker capabilities guaranteeing that the above mentioned class of automata is closed under the ...
Steve Kremer, Antoine Mercier 0002, Ralf Treinen
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Steve Kremer, Antoine Mercier 0002, Ralf Treinen
Comments (0)
books