Abstract
In the symbolic analysis of security protocols, two classical notions of knowledge, deducibility and indistinguishability, yield corresponding decision problems. We propose a procedure for both problems under arbitrary convergent equational theories. Our procedure terminates on a wide range of equational theories. In particular, we obtain a new decidability result for a theory we encountered when studying electronic voting protocols. We also provide a prototype implementation.
This work has been partly supported by the ANR SeSur AVOTÉ.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 387(1-2), 2–32 (2006)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. 28th ACM Symp. on Principles of Programming Languages (2001)
Anantharaman, S., Narendran, P., Rusinowitch, M.: Intruders with caps. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 20–35. Springer, Heidelberg (2007)
Armando, A., et al.: The AVISPA Tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: Proc. 21st IEEE Computer Security Foundations Symposium (CSF 2008) (2008)
Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: IEEE Symposium on Security and Privacy (S&P 2008). IEEE Comp. Soc. Press, Los Alamitos (2008)
Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: 12th ACM Conference on Computer and Communications Security (CCS 2005) (2005)
Baudet, M.: YAPA (Yet Another Protocol Analyzer) (2008), http://www.lsv.ens-cachan.fr/~baudet/yapa/index.html
Baudet, M., Cortier, V., Delaune, S.: YAPA: A generic tool for computing intruder knowledge. In: Treinen, R. (ed.) Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009), Brasília, Brazil, June-July 2009. LNCS. Springer, Heidelberg (to appear, 2009)
Chevalier, Y.: Résolution de problèmes d’accessibilité pour la compilation et la validation de protocoles cryptographiques. PhD thesis, Univ. Henri Poincaré (2003)
Ciobâcă, Ş.: KiSs (2009), http://www.lsv.ens-cachan.fr/~ciobaca/kiss
Ciobâcă, Ş., Delaune, S., Kremer, S.: Computing knowledge in security protocol under convergent equational theories. Research Report LSV-09-05, Laboratoire Spécification et Vérification, ENS Cachan, France, March 2009, 42 p. (2009)
Corin, R., Doumen, J., Etalle, S.: Analysing password protocol security against off-line dictionary attacks. In: Proc. 2nd International Workshop on Security Issues with Petri Nets and other Computational Models (WISP 2004). ENTCS (2004)
Cortier, V., Delaune, S.: Deciding knowledge in security protocols for monoidal equational theories. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 196–210. Springer, Heidelberg (2007)
Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security 14(1), 1–43 (2006)
Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security (to appear, 2008)
Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for the equational theory of Abelian groups with distributive encryption. Information and Computation 205(4), 581–623 (2007)
Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proc. 8th ACM Conference on Computer and Communications Security (CCS 2001) (2001)
Okamoto, T.: Receipt-free electronic voting schemes for large scale elections. In: Christianson, B., Lomas, M. (eds.) Security Protocols 1997. LNCS, vol. 1361. Springer, Heidelberg (1998)
Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions and composed keys is NP-complete. Theoretical Computer Science 299, 451–475 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ciobâcă, Ş., Delaune, S., Kremer, S. (2009). Computing Knowledge in Security Protocols under Convergent Equational Theories. In: Schmidt, R.A. (eds) Automated Deduction – CADE-22. CADE 2009. Lecture Notes in Computer Science(), vol 5663. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02959-2_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-02959-2_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02958-5
Online ISBN: 978-3-642-02959-2
eBook Packages: Computer ScienceComputer Science (R0)