# Deciding knowledge in security protocols under some e-voting theories

Mouhebeddine Berrima; Narjes Ben Rajeb; Véronique Cortier

RAIRO - Theoretical Informatics and Applications (2011)

- Volume: 45, Issue: 3, page 269-299
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topBerrima, Mouhebeddine, Ben Rajeb, Narjes, and Cortier, Véronique. "Deciding knowledge in security protocols under some e-voting theories." RAIRO - Theoretical Informatics and Applications 45.3 (2011): 269-299. <http://eudml.org/doc/222090>.

@article{Berrima2011,

abstract = {
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.
},

author = {Berrima, Mouhebeddine, Ben Rajeb, Narjes, Cortier, Véronique},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Security protocols; formal methods; decidability; e-voting;
equational theory; deduction; static equivalence; security protocols; equational theory},

language = {eng},

month = {9},

number = {3},

pages = {269-299},

publisher = {EDP Sciences},

title = {Deciding knowledge in security protocols under some e-voting theories},

url = {http://eudml.org/doc/222090},

volume = {45},

year = {2011},

}

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

DA - 2011/9//

PB - EDP Sciences

VL - 45

IS - 3

SP - 269

EP - 299

AB -
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.

LA - eng

KW - Security protocols; formal methods; decidability; e-voting;
equational theory; deduction; static equivalence; security protocols; equational theory

UR - http://eudml.org/doc/222090

ER -

## References

top- M. Abadi and V. Cortier, Deciding knowledge in security protocols under equational theories. Theoret. Comput. Sci.367 (2006) 2–32. Zbl1153.94339
- M. Abadi and C. Fournet, Mobile values, new names, and secure communication. SIGPLAN Not.36 (2001) 104–115. Zbl1323.68398
- 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. Zbl1081.68523
- 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. Zbl1148.68361
- 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. Zbl1242.94018
- 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).
- D. Chaum, Blind signatures for untraceable payments, in Proc. of the 8th Annual International Cryptology Conference (CRYPTO'82) (1982) 199–203. Zbl0521.94012
- 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. Zbl1068.68057
- Ş. 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). Zbl1250.03016
- 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.
- 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. Zbl1137.68325
- S. Delaune, Easy intruder deduction problems with homomorphisms. Inform. Process. Lett.97 (2006) 213–218. Zbl1184.68459
- 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. Zbl1284.68243
- S. Delaune, S. Kremer and M.D. Ryan, Verifying privacy-type properties of electronic voting protocols. J. Comput. Security17 (2009) 435–487. Zbl1284.68243
- 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. Zbl0992.68123
- 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. Zbl0188.04902
- 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). Zbl1078.68034
- 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). Zbl1092.68601
- D.A. McAllester, Automatic recognition of tractability in inference relations. J. ACM40 (1993) 284–303. Zbl0770.68106
- T. Okamoto, An electronic voting scheme, in Proc. of the 14th IFIP World Conference on IT Tools (1996) 21–30.
- 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. Zbl1042.68009

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.