Abstract
We present a new paradigm for unification arising out of a technique commonly used in cryptographic protocol analysis tools that employ unification modulo equational theories. This paradigm relies on: (i) a decomposition of an equational theory into (R,E) where R is confluent, terminating, and coherent modulo E, and (ii) on reducing unification problems to a set of problems \(s =_{}^{?} t\) under the constraint that t remains R/E-irreducible. We call this method asymmetric unification. We first present a general-purpose generic asymmetric unification algorithm. and then outline an approach for converting special-purpose conventional unification algorithms to asymmetric ones, demonstrating it for exclusive-or with uninterpreted function symbols. We demonstrate how asymmetric unification can improve performanceby running the algorithm on a set of benchmark problems. We also give results on the complexity and decidability of asymmetric unification.
S. Escobar and S. Santiago were partially supported by EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2010-21062-C02-02, and by Generalitat Valenciana PROMETEO2011/052. The following authors were partially supported by NSF: S. Escobar, J. Meseguer, and R. Sasse under CNS 09-04749 and CCF 09-05584; D. Kapur under CNS 09-05222; C. Lynch, Z. Liu, and C. Meadows under CNS 09-05378, and P. Narendran and S. Erbatur under CNS 09-05286. Part of the S. Erbatur’s work was supported while with the Department of Computer Science, University at Albany, and part of R. Sasse’s work was supported while with the Department of Computer Science, University of Illinois at Urbana-Champaign. Portions of this paper appeared in an abstract in the informal proceedings of UNIF’11.
One of the authors is an employee of the US government, and the rights of this work are transferred to the extent transferable according to title 17 U.S.C. 105.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
IEEE 802.11 Local and Metropolitan Area Networks: Wireless LAN Medium Access Control (MAC) and Physical (PHY) Specifications (1999)
Basin, D., Mödersheim, S., Viganò, L.: An on-the-fly model-checker for security protocol analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 253–270. Springer, Heidelberg (2003)
Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: CSFW, pp. 82–96. IEEE Computer Society (2001)
Bürckert, H.-J., Herold, A., Schmidt-Schauß, M.: On equational theories, unification, and (un)decidability. Journal of Symbolic Computation 8(1/2), 3–49 (1989)
Comon-Lundh, H., Delaune, S.: The finite variant property: How to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005)
Durán, F., Meseguer, J.: A Maude coherence checker tool for conditional order-sorted rewrite theories. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 86–103. Springer, Heidelberg (2010)
Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C., Meadows, C., Meseguer, J., Narendran, P., Santiago, S., Sasse, R.: Effective symbolic protocol analysis via equational irreducibility conditions. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 73–90. Springer, Heidelberg (2012)
Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C., Meadows, C., Meseguer, J., Narendran, P., Sasse, R.: Asymmetric unification: A new unification paradigm for cryptographic protocol analysis. In: UNIF 2011 (2011), https://sites.google.com/a/cs.uni.wroc.pl/unif-2011/program
Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program. 81(7-8), 898–928 (2012)
Harju, T., Karhumäki, J., Krob, D.: Remarks on generalized post correspondence problem. In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 39–48. Springer, Heidelberg (1996)
Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation - international edition, 2nd edn. Addison-Wesley (2003)
Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986)
Liu, Z., Lynch, C.: Efficient general unification for XOR with homomorphism. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 407–421. Springer, Heidelberg (2011)
Liu, Z.: Dealing Efficiently with Exclusive OR, Abelian Groups and Homomorphism in Cryptographic Protocol Analysis. PhD thesis, Clarkson University (2012), http://people.clarkson.edu/~clynch/papers/Dissertation_of_Zhiqiang_Liu.pdf
Lowe, G., Roscoe, A.W.R.: Using CSP to detect errors in the TMN protocol. IEEE Transactions on Software Engineering 23, 659–669 (1997)
Meseguer, J.: Conditional rewriting logic as a united model of concurrency. Theor. Comput. Sci. 96(1), 73–155 (1992)
Schmidt, B., Meier, S., Cremers, C.J.F., Basin, D.A.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Proc. CSF 2012, pp. 78–94. IEEE (2012)
Tatebayashi, M., Matsuzaki, N., Newman Jr., D.B.: Key distribution protocol for digital mobile communication systems. In: Brassard, G. (ed.) CRYPTO 1989. LNCS, vol. 435, pp. 324–334. Springer, Heidelberg (1990)
TeReSe, editor. Term Rewriting Systems. Cambridge University Press (2003)
Viry, P.: Equational rules for rewriting logic. Theor. Comp. Sci. 285(2), 487–517 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Erbatur, S. et al. (2013). Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. In: Bonacina, M.P. (eds) Automated Deduction – CADE-24. CADE 2013. Lecture Notes in Computer Science(), vol 7898. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38574-2_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-38574-2_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38573-5
Online ISBN: 978-3-642-38574-2
eBook Packages: Computer ScienceComputer Science (R0)