Deciding knowledge in security protocols under some e-voting theories
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 45 (2011) no. 3, pp. 269-299.

In the last decade, formal methods have proved their interest when analyzing security protocols. Security protocols require in particular to reason about the attacker knowledge. Two standard notions are often considered in formal approaches: deducibility and indistinguishability relations. The first notion states whether an attacker can learn the value of a secret, while the latter states whether an attacker can notice some difference between protocol runs with different values of the secret. Several decision procedures have been developed so far for both notions but none of them can be applied in the context of e-voting protocols, which require dedicated cryptographic primitives. In this work, we show that both deduction and indistinguishability are decidable in polynomial time for two theories modeling the primitives of e-voting protocols.

DOI : https://doi.org/10.1051/ita/2011119
Classification : 68Q85
Mots clés : security protocols, formal methods, decidability, e-voting, equational theory, deduction, static equivalence
@article{ITA_2011__45_3_269_0,
     author = {Berrima, Mouhebeddine and Ben Rajeb, Narjes and Cortier, V\'eronique},
     title = {Deciding knowledge in security protocols under some e-voting theories},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {269--299},
     publisher = {EDP-Sciences},
     volume = {45},
     number = {3},
     year = {2011},
     doi = {10.1051/ita/2011119},
     zbl = {1223.68016},
     mrnumber = {2836490},
     language = {en},
     url = {http://www.numdam.org/articles/10.1051/ita/2011119/}
}
TY  - JOUR
AU  - Berrima, Mouhebeddine
AU  - Ben Rajeb, Narjes
AU  - Cortier, Véronique
TI  - Deciding knowledge in security protocols under some e-voting theories
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2011
DA  - 2011///
SP  - 269
EP  - 299
VL  - 45
IS  - 3
PB  - EDP-Sciences
UR  - http://www.numdam.org/articles/10.1051/ita/2011119/
UR  - https://zbmath.org/?q=an%3A1223.68016
UR  - https://www.ams.org/mathscinet-getitem?mr=2836490
UR  - https://doi.org/10.1051/ita/2011119
DO  - 10.1051/ita/2011119
LA  - en
ID  - ITA_2011__45_3_269_0
ER  - 
Berrima, Mouhebeddine; Ben Rajeb, Narjes; Cortier, Véronique. Deciding knowledge in security protocols under some e-voting theories. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 45 (2011) no. 3, pp. 269-299. doi : 10.1051/ita/2011119. http://www.numdam.org/articles/10.1051/ita/2011119/

[1] M. Abadi and V. Cortier, Deciding knowledge in security protocols under equational theories. Theoret. Comput. Sci. 367 (2006) 2-32. | MR 2272703 | Zbl 1153.94339

[2] M. Abadi and C. Fournet, Mobile values, new names, and secure communication. SIGPLAN Not. 36 (2001) 104-115.

[3] A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P.H. Drielsma, P.-C. Héam, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. Von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganò and L. Vigneron, The AVISPA Tool for the automated validation of internet security protocols and applications, in Proc. of the 17th International Conference on Computer Aided Verification, CAV'2005. Lect. Notes Comput. Sci. 3576 (2005) 281-285. | Zbl 1081.68523

[4] M. Arnaud, V. Cortier and S. Delaune, Combining algorithms for deciding knowledge in security protocols, in Proc. of the 6th International Symposium on Frontiers of Combining Systems (FroCoS'2007). Lect. Notes Comput. Sci. 4720 (2007) 103-117. | Zbl 1148.68361

[5] M. Baudet, V. Cortier and S. Delaune, YAPA: A generic tool for computing intruder knowledge, in Proc. of the 20th International Conference on Rewriting Techniques and Applications (RTA'09). Lect. Notes Comput. Sci. 5595 (2009) 148-163. | MR 2545475 | Zbl 1242.94018

[6] B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, in Proc. of the 14th Computer Security Foundations Workshop CSFW'01. IEEE Computer Society Press (2001).

[7] D. Chaum, Blind signatures for untraceable payments, in Proc. of the 8th Annual International Cryptology Conference (CRYPTO'82) (1982) 199-203. | Zbl 0521.94012

[8] Y. Chevalier, R. Kusters, M. Rusinowitch and M. Turuani, An NP decision procedure for protocol insecurity with XOR. Theoret. Comput. Sci. 338 (2005) 247-274. | MR 2141523 | Zbl 1068.68057

[9] Ş. Ciobâcă, S. Delaune and S. Kremer, Computing knowledge in security protocols under convergent equational theories, in Proc. of the 22nd International Conference on Automated Deduction (CADE'09) (2009). | Zbl 1250.03016

[10] H. Comon-Lundh and V. Shmatikov, Intruder deductions, constraint solving and insecurity decision in presence of exclusive or, in Proc. of the 18th Annual IEEE Syposium on Logic in Computer Science (LICS-03). IEEE Computer Society (2003) 271-280. | Zbl 1201.68049

[11] V. Cortier and S. Delaune, Deciding knowledge in security protocols for monoidal equational theories, in Proc. of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07). Lect. Notes Artif. Int. 4790 (2007) 196-210. | Zbl 1137.68325

[12] S. Delaune, Easy intruder deduction problems with homomorphisms. Inform. Process. Lett. 97 (2006) 213-218. | MR 2196854 | Zbl 1184.68459

[13] S. Delaune, S. Kremer and M.D. Ryan, Verifying properties of electronic voting protocols, in Proc. of the IAVoSS Workshop On Trustworthy Elections (WOTE'06) (2006) 45-52.

[14] S. Delaune, S. Kremer and M.D. Ryan, Verifying privacy-type properties of electronic voting protocols. J. Comput. Security 17 (2009) 435-487. | Zbl 1284.68243

[15] N. Dershowitz and D.A. Plaisted, Rewriting, in Handbook of Automated Reasoning. J.A. Robinson and A. Voronkov, Eds. Elsevier and MIT Press (2001) 535-610. | Zbl 0992.68123

[16] D.E. Knuth and P.B. Bendix, Simple word problems in universal algebras, in Computational Problems in Abstract Algebra. J. Leech, Eds. Pergamon Press (1970) 263-297. | MR 255472 | Zbl 0188.04902

[17] P. Lafourcade, D. Lugiez and R. Treinen, Intruder deduction for AC-like equational theories with homomorphisms, in Proc. of the 16th International Conference on Rewriting Techniques and Applications (RTA'05). Springer (2005). | MR 2184554 | Zbl 1078.68034

[18] B. Lee, C. Boyd, E. Dawson, K. Kim, J. Yang and S. Yoo, Providing receipt-freeness in mixnet-based voting protocols, in Proc. of the 6th International Conference on Information Security and Cryptology (ICISC'03). Springer (2003). | MR 2093712 | Zbl 1092.68601

[19] D.A. Mcallester, Automatic recognition of tractability in inference relations. J. ACM 40 (1993) 284-303. | MR 1217880 | Zbl 0770.68106

[20] T. Okamoto, An electronic voting scheme, in Proc. of the 14th IFIP World Conference on IT Tools (1996) 21-30.

[21] M. Rusinowitch and M. Turuani, Protocol insecurity with finite number of sessions is NP-complete, in Proc. of the 14th Computer Security Foundations Workshop (CSFW'01). IEEE Computer Society Press (2001) 174-190.

Cité par Sources :