Abstract
Analysis of authentication cryptographic protocols, particularly finding flaws in them and determining a sequence of actions that an intruder can take to gain access to the information which a given protocol purports not to reveal, has recently received considerable attention. One effective way of detecting flaws is to hypothesize an insecure state and determine whether it is possible to get to that state by a legal sequence of actions permitted by the protocol from some legal initial state which captures the knowledge of the principals and the assumptions made about an intruder’s behavior. Relations among encryption and decryption functions as well as properties of number theoretic functions used in encryption and decryption can be specified as rewrite rules. This, for example, is the approach used by the NRL Protocol Analyzer, which uses narrowing to reason about such properties of cryptographic and number-theoretic functions.
Following [15], a related approach is proposed here in which equation solving modulo most of these properties of cryptographic and number-theoretic functions is done by developing new unification algorithms for such theories. A new unification algorithm for an equational theory needed to reason about protocols that use the Diffie-Hellman algorithm is developed. In this theory, multiplication forms an abelian group; exponentiation function distributes over multiplication, and exponents can commute. This theory is useful for analyzing protocols which use blinded signatures. It is proved that the unification problem over this equational theory can be reduced to the unification problem modulo the theory of abelian groups with commuting homomorphisms with an additional constraint. Baader’s unification algorithm for the theory of abelian groups with commuting homomorphisms, which reduces the unification problem to solving equations over the polynomial ring over the integers with the commuting homomorphisms serving as indeterminates, is generalized to give a unification algorithm over the theory of abelian groups with commuting homomorphism with a linear constraint.
It is also shown that the unification problem over a (simple) extension of the equational theory considered here (which is also an extension of the equational theory considered in [15]) is undecidable.
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
Baader, F., Schultz, K.U.: Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 50–65. Springer, Heidelberg (1992)
Baader, F.: Unification in Commutative Theories, Hilbert’s Basis Theorem, and Gröbner Bases. J. ACM 40(3), 477–503 (1993)
Baader, F., Nutt, W.: Adding Homomorphisms to Commutative/Monoidal Theories, or: How Algebra Can Help in Equational Unification. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 124–135. Springer, Heidelberg (1991)
Baader, F., Snyder, W.: Unification Theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier Science Publishers, Amsterdam (2001)
Buchberger, B.: Gröbner Bases: An Algorithmic Method in Polynomial Ideal Theory. In: Bose, N.K. (ed.) Multidimensional Systems Theory, Reichel, Dordrecht, pp. 184–229 (1985)
Chaum, D.: Security without Identification: Transaction Systems to Make Big Brother Obsolete. CACM 28(10), 1030–1044 (1985)
Clark, J., Jacob, J.: A Survey of Authentication Protocol Literature: Version 1.0. Unpublished Technical Report, Department of Computer Science, University of York, UK (November 1997), Available at the http://www-users.cs.york.ac.uk/~jac/papers/drareviewps.ps
Davis, M.: Computability and Unsolvability. Dover Publications, Mineola (1982)
Hullot, J.-M.: Canonical forms and unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980)
Kandri-Rody, A., Kapur, D.: Computing the Gröbner Basis of a Polynomial Ideal over Integers. In: Proc. Third MACSYMA Users’ Conference, Schenectady, NY, pp. 436–451 (July 1984)
Kapur, D., Narendran, P., Wang, L.: A Unification Algorithm for Analysis of Protocols with Blinded Signatures. Technical Report, Department of Computer Science, University at Albany–SUNY, Albany, NY. Also: Technical Report, Department of Computer Science, University of New Mexico, Albuquerque, NM (July 2002)
Kapur, D., Sivakumar, G.: A Total, Ground Path Ordering for Proving Termination of AC-Rewrite Systems. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 142–156. Springer, Heidelberg (1997)
Meadows, C.: Formal Verification of Cryptographic Protcols: A Survey. In: Kim, K.-c., Matsumoto, T. (eds.) ASIACRYPT 1996. LNCS, vol. 1163. Springer, Heidelberg (1996)
Meadows, C.: The NRL Protocol Analyzer: An Overview. J. Logic Programming 26(2), 113–131 (1996)
Meadows, C., Narendran, P.: A Unification Algorithm for the Group Diffie- Hellman Protocol. Presented at the Workshop on Issues in the Theory of Security (WITS 2002), Portland, Oregon (January 2002)
Narendran, P., Pfenning, F., Statman, R.: On the Unification Problem for Cartesian Closed Categories. Journal of Symbolic Logic 62(2), 636–647 (1997)
Nutt, W.: Unification in Monoidal Theories. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449. Springer, Heidelberg (1990)
Pereira, O., Quisquater, J.-J.: A Security Analysis of the Cliques Protocols Suites. In: Proc. 14th IEEE Computer Security Foundations Workshop, pp. 73–81 (June 2001)
Rivest, R.L., Shamir, A., Adleman, L.: A Method for Obtaining Digital Signatures and Public Key Cryptosystems. CACM 21(2), 120–126 (1978)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Kapur, D., Narendran, P., Wang, L. (2005). A Unification Algorithm for Analysis of Protocols with Blinded Signatures. In: Hutter, D., Stephan, W. (eds) Mechanizing Mathematical Reasoning. Lecture Notes in Computer Science(), vol 2605. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32254-2_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-32254-2_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25051-7
Online ISBN: 978-3-540-32254-2
eBook Packages: Computer ScienceComputer Science (R0)