کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
422522 | 685101 | 2007 | 21 صفحه PDF | دانلود رایگان |

The first step in the verification of cryptographic protocols is to decide the intruder deduction problem, that is the vulnerability to a so-called passive attacker. We extend the Dolev-Yao model in order to model this problem in presence of the equational theory of a commutative encryption operator which distributes over the exclusive-or operator. The interaction between the commutative distributive law of the encryption and exclusive-or offers more possibilities to decrypt an encrypted message than in the non-commutative case, which imply a more careful analysis of the proof system. We prove decidability of the intruder deduction problem for a commutative encryption which distributes over exclusive-or with a DOUBLE-EXP-TIME procedure. And we obtain that this problem is EXPSPACE-hard in the binary case.
Journal: Electronic Notes in Theoretical Computer Science - Volume 171, Issue 4, 10 July 2007, Pages 37-57