Hostname: page-component-cd9895bd7-mkpzs Total loading time: 0 Render date: 2024-12-24T03:17:32.980Z Has data issue: false hasContentIssue false
  • English
  • Français

Deciding knowledge in security protocols under some e-voting theories

Published online by Cambridge University Press:  26 August 2011

Mouhebeddine Berrima ,
Narjes Ben Rajeb  and
Véronique Cortier
Mouhebeddine Berrima
Affiliation:
LIP2, Faculté des Sciences, Tunis, Tunisia. [email protected]
Narjes Ben Rajeb
Affiliation:
LIP2, Institut National des Sciences Appliquées et de Technologie, Tunis, Tunisia.
Véronique Cortier
Affiliation:
Loria, INRIA & CNRS, Nancy, France.
Get access

Abstract

In the last decade, formal methods have proved their interest whenanalyzing security protocols. Security protocols require inparticular to reason about the attacker knowledge. Two standardnotions are often considered in formal approaches: deducibility andindistinguishability relations. The first notion states whether anattacker can learn the value of a secret, while the latter stateswhether an attacker can notice some difference between protocol runswith different values of the secret. Several decision procedureshave been developed so far for both notions but none of them can beapplied in the context of e-voting protocols, which requirededicated cryptographic primitives. In this work, we show that bothdeduction and indistinguishability are decidable in polynomial timefor two theories modeling the primitives of e-voting protocols.

Keywords

Security protocolsformal methodsdecidabilitye-votingequational theorydeductionstatic equivalence
Type
Research Article
Information
RAIRO - Theoretical Informatics and Applications , Volume 45 , Issue 3 , July 2011 , pp. 269 - 299
Copyright
© EDP Sciences, 2011

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abadi, M. and Cortier, V., Deciding knowledge in security protocols under equational theories. Theoret. Comput. Sci. 367 (2006) 2–32. CrossRef
Abadi, M. and Fournet, C., Mobile values, new names, and secure communication. SIGPLAN Not. 36 (2001) 104–115. CrossRef
Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., Héam, P.-C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L. and Vigneron, L., Tool, The AVISPA 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. CrossRef
Arnaud, M., Cortier, V. and Delaune, S., 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. CrossRef
Baudet, M., Cortier, V. and Delaune, S., 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. CrossRef
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.
Chevalier, Y., Kusters, R., Rusinowitch, M. and Turuani, M., NP de, Ancision procedure for protocol insecurity with XOR. Theoret. Comput. Sci. 338 (2005) 247–274. CrossRef
Ş. 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).
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.
Cortier, V. and Delaune, S., 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.
Delaune, S., Easy intruder deduction problems with homomorphisms. Inform. Process. Lett. 97 (2006) 213–218. CrossRef
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.
Delaune, S., Kremer, S. and Ryan, M.D., Verifying privacy-type properties of electronic voting protocols. J. Comput. Security 17 (2009) 435–487. CrossRef
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.
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.
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).
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).
McAllester, D.A., Automatic recognition of tractability in inference relations. J. ACM 40 (1993) 284–303. CrossRef
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.