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}, }