PhD defense of Sergiu Bursuc
Title
Deducibility constraints in a quotient algebra: reduction of models and applications to security
Time and place
December, 1st, 17.30, Salle Condorcet, ENS de Cachan
Jury
Abstract
To enable formal and automated analysis of security protocols, one has
to abstract implementations of cryptographic primitives by terms in a
given algebra. However, the algebra can not be free, as cryptographic
primitives have algebraic properties that are either relevant to their
specification or else they can be simply observed in implementations at
hand. These properties are sometimes essential for the execution of the
protocol, but they also open the possibility for an attack, as they
give to an intruder the means to deduce new information from the
messages that he intercepts over the network.
In consequence, there was much work over the last few years towards
enriching the Dolev-Yao model, originally based on a free algebra, with
algebraic properties, modelled by equational theories. In this context,
we have been interested in general decision procedures for the
insecurity of protocols, that can be applied to classes of equational
theories.
First, we propose a way to simplify the equational theory, based
on an appropriate definition of alien subterms of a term. From this, we
derive a decision procedure for a non-trivial combination of Abelian
group properties, exponentiation and homomorphism. This theory was used
for modelling an electronic purse protocol by France Telecom. Previously
known techniques were not applicable, as the theory was a too intricate
combination of sub-theories.
Next, we show that constraint systems, that represent all possible
traces of a protocol, can be simplified in an uniform and systematic
way, when the equational theory does not contain
Associative-Commutative symbols. This allows for a symbolic
representation of all traces of a protocol as a set of solved forms.
The main property of the equational theory that ensures the
completeness of the proposed simplification procedure is saturation
with respect to ordered resolution. When the saturated theory is
finite, the set of solved forms is finite as well and permits deciding
any trace property, in particular the secrecy of a message. When the
saturated theory is infinite, one needs to group solved forms together,
by introducing a new predicate, in order to obtain a finite
representation of all solutions of the original system. This has been
done for the particular case of blind signatures and is yet to be
understood in a more general setting.
Manuscript
Here