Stéphanie Delaune, Pascal Lafourcade, Denis Lugiez, and Ralf Treinen. Symbolic Protocol Analysis in Presence of a Homomorphism Operator and *Exclusive Or*. In * Proceedings of the 33rd International Colloquium on Automata, Languages and Programming (ICALP'06) --- Part II*, pp. 132–143, Lecture Notes in Computer Science 4052, Springer, Venice, Italy, July 2006.

Security of a cryptographic protocol for a bounded number of sessions is usually expressed as a symbolic trace reachability problem. We show that symbolic trace reachability for well-defined protocols is decidable in presence of the exclusive or theory in combination with the homomorphism axiom. These theories allow us to model basic properties of important cryptographic operators. This trace reachability problem can be expressed as a system of symbolic deducibility constraints for a certain inference system describing the capabilities of the attacker. One main step of our proof consists in reducing deducibility constraints to constraints for deducibility in one step of the inference system. This constraint system, in turn, can be expressed as a system of quadratic equations of a particular form over \(\mathbbZ/2\mathbbZ[h]\), the ring of polynomials in one indeterminate over the finite field \(\mathbbZ/2\mathbbZ\). We show that satisfiability of such systems is decidable.

@inproceedings{DLLT-ICALP2006, abstract = {Security of a cryptographic protocol for a bounded number of sessions is usually expressed as a symbolic trace reachability problem. We show that symbolic trace reachability for well-defined protocols is decidable in presence of the exclusive or theory in combination with the homomorphism axiom. These theories allow us to model basic properties of important cryptographic operators. This trace reachability problem can be expressed as a system of symbolic deducibility constraints for a certain inference system describing the capabilities of the attacker. One main step of our proof consists in reducing deducibility constraints to constraints for deducibility in one step of the inference system. This constraint system, in turn, can be expressed as a system of quadratic equations of a particular form over \(\mathbb{Z}/2\mathbb{Z}[h]\), the ring of polynomials in one indeterminate over the finite field \(\mathbb{Z}/2\mathbb{Z}\). We show that satisfiability of such systems is decidable.}, address = {Venice, Italy}, author = {Delaune, St{\'e}phanie and Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf}, booktitle = {{P}roceedings of the 33rd {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'06)~--- {P}art~{II}}, OPTDOI = {10.1007/11787006_12}, editor = {Buglesi, Michele and Preneel, Bart and Sassone, Vladimiro and Wegener, Ingo}, month = jul, pages = {132-143}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Symbolic Protocol Analysis in Presence of a Homomorphism Operator and {\emph{Exclusive~Or}}}, volume = {4052}, year = {2006}, acceptrate = {24/81}, acronym = {{ICALP}'06}, nmonth = {7}, lsv-category = {intc}, wwwpublic = {public and ccsb}, }