Abstract
When formally analyzing security protocols it is often important to express properties in terms of an adversary’s inability to distinguish two protocols. It has been shown that this problem amounts to deciding the equivalence of two constraint systems, i.e., whether they have the same set of solutions. In this paper we study this equivalence problem when cryptographic primitives are modeled using a group equational theory, a special case of monoidal equational theories. The results strongly rely on the isomorphism between group theories and rings. This allows us to reduce the problem under study to the problem of solving systems of equations over rings. We provide several new decidability and complexity results, notably for equational theories which have applications in security protocols, such as exclusive or and Abelian groups which may additionally admit a unary, homomorphic symbol.
The research leading to these results has received funding from the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement n° 258865, project ProSecure, and the project JCJC VIP ANR-11-JS02-006.
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 Symposium on Principles of Programming Languages (POPL 2001), pp. 104–115. ACM Press (2001)
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Inf. Comput. 148(1), 1–70 (1999)
Arapinis, M., Chothia, T., Ritter, E., Ryan, M.D.: Analysing unlinkability and anonymity using the applied pi calculus. In: Proc. 23rd Computer Security Foundations Symposium (CSF 2010), pp. 107–121. IEEE Comp. Soc. Press (2010)
Armando, A., Carbone, R., Compagna, L., Cuéllar, J., Tobarra, M.L.: Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for google apps. In: Proc. 6th ACM Workshop on Formal Methods in Security Engineering (FMSE 2008), pp. 1–10. ACM Press (2008)
Baader, F.: Unification in commutative theories. Journal of Symbolic Computation 8(5), 479–497 (1989)
Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proc. 12th Conference on Computer and Communications Security (CCS 2005), pp. 16–25. ACM Press (2005)
Cheval, V., Comon-Lundh, H., Delaune, S.: Automating Security Analysis: Symbolic Equivalence of Constraint Systems. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 412–426. Springer, Heidelberg (2010)
Chevalier, Y., Rusinowitch, M.: Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures. Theoretical Computer Science 411(10), 1261–1282 (2010)
Chevalier, Y., Rusinowitch, M.: Decidability of equivalence of symbolic derivations. J. Autom. Reasoning 48(2), 263–292 (2012)
Comon-Lundh, H., Cortier, V., Zalinescu, E.: Deciding security properties of cryptographic protocols. application to key cycles. Transaction on Computational Logic 11(2) (2010)
Cortier, V., Delaune, S.: Decidability and combination results for two notions of knowledge in security protocols. J. of Autom. Reasoning 48(4), 441–487 (2012)
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.: Easy intruder deduction problems with homomorphisms. Information Processing Letters 97(6), 213–218 (2006)
Delaune, S., Kremer, S., Pasaila, D.: Security protocols, constraint systems, and group theories. Research Report LSV-12-06, Laboratoire Spécification et Vérification, ENS Cachan, France, 23 pages (2012)
Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security 17(4), 435–487 (2009)
Delaune, S., Lafourcade, P., Lugiez, D., Treinen, R.: Symbolic protocol analysis for monoidal equational theories. Inf. Comp. 206(2-4), 312–351 (2008)
Lafourcade, P., Lugiez, D., Treinen, R.: Intruder Deduction for AC-Like Equational Theories with Homomorphisms. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 308–322. Springer, Heidelberg (2005)
Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proc. 8th ACM Conference on Computer and Communications Security (CCS 2001). ACM Press (2001)
Nutt, W.: Unification in Monoidal Theories. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 618–632. Springer, Heidelberg (1990)
Schrijver, A.: Theory of Linear and Integer Programming. Wiley (1986)
Tiu, A., Dawson, J.: Automating open bisimulation checking for the spi-calculus. In: Proc. 23rd Computer Security Foundations Symposium (CSF 2010), pp. 307–321. IEEE Comp. Soc. Press (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Delaune, S., Kremer, S., Pasaila, D. (2012). Security Protocols, Constraint Systems, and Group Theories. In: Gramlich, B., Miller, D., Sattler, U. (eds) Automated Reasoning. IJCAR 2012. Lecture Notes in Computer Science(), vol 7364. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31365-3_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-31365-3_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31364-6
Online ISBN: 978-3-642-31365-3
eBook Packages: Computer ScienceComputer Science (R0)