Sergiu Bursuc, Hubert Comon-Lundh, and Stéphanie Delaune. Deducibility Constraints, Equational Theory and Electronic Money. In Rewriting, Computation and Proof --- Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of his 60th Birthday, pp. 196–212, Lecture Notes in Computer Science 4600, Springer, Cachan, France, June 2007.
The starting point of this work is a case study (from France Télécom) of an electronic purse protocol. The goal was to prove that the protocol is secure or that there is an attack. Modeling the protocol requires algebraic properties of a fragment of arithmetic, typically containing modular exponentiation. The usual equational theories described in papers on security protocols are too weak: the protocol cannot even be executed in these models. We consider here an equational theory which is powerful enough for the protocol to be executed, and for which unification is still decidable.
Our main result is the decidability of the so-called intruder deduction problem, i.e., security in presence of a passive attacker, taking the algebraic properties into account. Our equational theory is a combination of several equational theories over non-disjoint signatures.
@inproceedings{BCD-jouannaud,
abstract = {The starting point of this work is a case study (from
France T\'el\'ecom) of an electronic purse protocol.
The~goal was to prove that the protocol is secure or
that there is an attack. Modeling the protocol
requires algebraic properties of a fragment of
arithmetic, typically containing modular
exponentiation. The~usual equational theories
described in papers on security protocols are too
weak: the~protocol cannot even be executed in these
models. We~consider here an equational theory which
is powerful enough for the protocol to be executed,
and for which unification is still decidable.\par Our
main result is the decidability of the so-called
intruder deduction problem, i.e.,~security in
presence of a passive attacker, taking the algebraic
properties into account. Our~equational theory is a
combination of several equational theories over
non-disjoint signatures.},
address = {Cachan, France},
author = {Bursuc, Sergiu and Comon{-}Lundh, Hubert and
Delaune, St{\'e}phanie},
booktitle = {{R}ewriting, {C}omputation and {P}roof~--- {E}ssays
{D}edicated to {J}ean-{P}ierre {J}ouannaud on the
{O}ccasion of his 60th {B}irthday},
OPTDOI = {10.1007/978-3-540-73147-4_10},
editor = {Comon{-}Lundh, Hubert and Kirchner, Claude and
Kirchner, H{\'e}l{\`e}ne},
month = jun,
pages = {196-212},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Deducibility Constraints, Equational Theory and
Electronic Money},
volume = {4600},
year = {2007},
acronym = {{R}ewriting, {C}omputation and {P}roof},
nmonth = {6},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}