Proving Group Protocols Secure Against Eavesdroppers
Steve Kremer, Antoine Mercier, and Ralf Treinen. Proving Group Protocols Secure Against Eavesdroppers. In Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR'08), pp. 116–131, Lecture Notes in Artificial Intelligence 5195, Springer-Verlag, Sydney, Australia, August 2008.
doi:10.1007/978-3-540-71070-7_9
Download
[PDF] [PDF (long version)] [HTML]
Abstract
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 application of the remaining attacker rules. The class of protocols respecting these restrictions is large enough to cover several existing protocols, such as the GDH family, GKE, and others.
BibTeX
@inproceedings{KMT-ijcar08,
abstract = {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
\emph{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.\par 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 \textit{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 application of the
remaining attacker rules. The class of protocols
respecting these restrictions is large enough to
cover several existing protocols, such as the GDH
family, GKE, and others.},
address = {Sydney, Australia},
author = {Kremer, Steve and Mercier, Antoine and Treinen, Ralf},
booktitle = {{P}roceedings of the 4th {I}nternational {J}oint
{C}onference on {A}utomated {R}easoning ({IJCAR}'08)},
DOI = {10.1007/978-3-540-71070-7_9},
editor = {Armando, Alessandro and Baumgartner, Peter and
Dowek, Gilles},
month = aug,
pages = {116-131},
publisher = {Springer-Verlag},
series = {Lecture Notes in Artificial Intelligence},
title = {Proving Group Protocols Secure Against Eavesdroppers},
volume = {5195},
year = {2008},
acceptrate = {26/80},
acronym = {{IJCAR}'08},
nmonth = {8},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-ijcar08.pdf},
}