Abstract
We describe a method for enumerating all essentially different executions possible for a cryptographic protocol. We call them the shapes of the protocol. Naturally occurring protocols have only finitely many, indeed very few shapes. Authentication and secrecy properties are easy to determine from them, as are attacks. cpsa, our Cryptographic Protocol Shape Analyzer, implements the method.
In searching for shapes, cpsa starts with some initial behavior, and discovers what shapes are compatible with it. Normally, the initial behavior is the point of view of one participant. The analysis reveals what the other principals must have done, given this participant’s view.
Supported by the National Security Agency and by MITRE-Sponsored Research.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. Journal of the ACM 52(1), 102–146 (2005)
Amadio, R.M., Lugiez, D.: On the reachability problem in cryptographic protocols. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 380–394. Springer, Heidelberg (2000)
Backes, M., Pfitzmann, B.: Relating cryptographic and symbolic key secrecy. In: Proceedings, 26th IEEE Symposium on Security and Privacy (May 2005), Extended version, http://eprint.iacr.org/2004/300
Blanchet, B., Podelski, A.: Verification of cryptographic protocols: Tagging enforces termination. In: Gordon, A.D. (ed.) ETAPS 2003 and FOSSACS 2003. LNCS, vol. 2620, pp. 136–152. Springer, Heidelberg (2003)
Canetti, R., Herzog, J.C.: Universally Composable Symbolic Analysis of Mutual Authentication and Key-Exchange Protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 380–403. Springer, Heidelberg (2006)
Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Searching for shapes in cryptographic protocols (extended version) (November 2006), http://eprint.iacr.org/2006/435
Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Transactions on Information Theory 29, 198–208 (1983)
Durgin, N., et al.: Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security 12(2), 247–311 (2004)
Gordon, A.D., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. Journal of Computer Security 12(3-4), 435–484 (2003)
Guttman, J.D., Thayer, F.J.: Authentication tests and the structure of bundles. Theoretical Computer Science 283(2), 333–380 (2002), Conference version appeared in IEEE Symposium on Security and Privacy (May 2000)
Herzog, J.C.: The Diffie-Hellman key-agreement scheme in the strand-space model. In: 16th Computer Security Foundations Workshop, Asilomar, CA, June 2003, pp. 234–247. IEEE Computer Society Press, Los Alamitos (2003)
ITU. Message sequence chart (MSC). Recommendation Z.120 (1999)
Lamport, L.: Time, clocks and the ordering of events in a distributed system. CACM 21(7), 558–565 (1978)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: 8th ACM Conference on Computer and Communications Security (CCS ’01), pp. 166–175. ACM Press, New York (2001)
Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12) (1978)
Paulson, L.C.: Relations between secrets: Two formal analyses of the Yahalom protocol. Journal of Computer Security (2001)
Perrig, A., Song, D.X.: Looking for diamonds in the desert: Extending automatic protocol generation to three-party authentication and key agreement protocols. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop, July 2000, IEEE Computer Society Press, Los Alamitos (2000)
Ramanujam, R., Suresh, S.P.: Decidability of context-explicit security protocols. Journal of Computer Security 13(1), 135–166 (2005), Preliminary version appeared in WITS ’03, Workshop on Issues in the Theory of Security, Warsaw (April 2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Doghmi, S.F., Guttman, J.D., Thayer, F.J. (2007). Searching for Shapes in Cryptographic Protocols. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_41
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_41
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)