@article{LLT07,
title = { Intruder Deduction for the Equational Theory of {A}belian Groups with Distributive Encryption },
author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
month = {apr},
year = {2007},
journal = {Information and Computation},
number = {4},
pages = {581-623},
publisher = {Elsevier Science Publishers},
volume = {205},
team = {DCS},
abstract = {Cryptographic protocols are small programs which involve a high level of concurrency and which are difficult to analyze by hand. The~most successful methods to verify such protocols are based on rewriting techniques and automated deduction in order to implement or mimic the process calculus describing the execution of a protocol. We~are interested in the intruder deduction problem, that is vulnerability to passive attacks in presence of equational theories which model the protocol specification and properties of the cryptographic operators.\par In the present paper we consider the case where the encryption distributes over the operator of an Abelian group or over an exclusive-or operator. We~prove decidability of the intruder deduction problem in both cases. We~obtain a PTIME decision procedure in a restricted case, the so-called binary case.\par These decision procedures are based on a careful analysis of the proof system modeling the deductive power of the intruder, taking into account the algebraic properties of the equational theories under consideration. The~analysis of the deduction rules interacting with the equational theory relies on the manipulation of \(\mathbb{Z}\)-modules in the general case, and on results from prefix rewriting in the binary case.},
}
