Abstract
Although cryptographic protocols are typically analyzed in isolation, they are used in combinations. If a protocol Π 1, when analyzed alone, was shown to meet some security goals, will it still meet those goals when executed together with a second protocol Π 2? Not necessarily: for every Π 1, some Π 2s undermine its goals. We use the strand space “authentication test” principles to suggest a criterion to ensure a Π 2 preserves Π 1’s goals; this criterion strengthens previous proposals.
Security goals for Π 1 are expressed in a language \(\mathcal{L}\)(Π 1) in classical logic. Strand spaces provide the models for \(\mathcal{L}\)(Π 1). Certain homomorphisms among models for \(\mathcal{L}\)(Π) preserve the truth of the security goals. This gives a way to extract—from a counterexample to a goal that uses both protocols—a counterexample using only the first protocol. This model-theoretic technique, using homomorphisms among models to prove results about a syntactically defined set of formulas, appears to be novel for protocol analysis.
Supported 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
Andova, S., Cremers, C.J.F., Gjøsteen, K., Mauw, S., Mjølsnes, S.F., Radomirović, S.: Sufficient conditions for composing security protocols. Information and Computation (2007)
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 (2008)
Backes, M., Pfitzmann, B.: Relating cryptographic and symbolic key secrecy. In: Proceedings of 26th IEEE Symposium on Security and Privacy (May 2005)
Balacheff, B., Chen, L., Pearson, S., Plaquin, D., Proudler, G.: Trusted Computing Platforms: TCPA Technology in Context. Prentice Hall PTR, NJ (2003)
Brickell, E., Camenisch, J., Chen, L.: Direct anonymous attestation. In: ACM Conference on Communications and Computer Security (CCS) (2004)
Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: FOCS, IACR 2000/067 (October 2001)
Canetti, R., Herzog, J.: 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)
Cortier, V., Delaitre, J., Delaune, S.: Safely composing security protocols. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 352–363. Springer, Heidelberg (2007)
Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositional logic for security protocols. Journal of Computer Security 13(3), 423–482 (2005)
Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Completeness of the authentication tests. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 106–121. Springer, Heidelberg (2007)
Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Searching for shapes in cryptographic protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523–537. Springer, Heidelberg (2007), Extended version, 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., Lincoln, P., Mitchell, J., Scedrov, A.: Multiset rewriting and the complexity of bounded security protocols. Journal of Computer Security 12(2), 247–311 (2004)
Fröschle, S.: Adding branching to the strand space model. In: Proceedings of EXPRESS 2008. Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (2008)
Goguen, J.A., Meseguer, J.: Order-sorted algebra I. Theoretical Computer Science 105(2), 217–273 (1992)
Guttman, J.D., Herzog, J.C., Ramsdell, J.D., Sniffen, B.T.: Programming cryptographic protocols. In: De Nicola, R., Sangiorgi, D. (eds.) TGC 2005. LNCS, vol. 3705, pp. 116–145. Springer, Heidelberg (2005)
Guttman, J.D., Thayer, F.J.: Protocol independence through disjoint encryption. In: Proceedings of 13th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2000)
Guttman, J.D., Thayer, F.J.: Authentication tests and the structure of bundles. Theoretical Computer Science 283(2), 333–380 (2002)
Heather, J., Lowe, G., Schneider, S.: How to prevent type flaw attacks on security protocols. In: Proceedings of 13th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2000)
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
Guttman, J.D. (2009). Cryptographic Protocol Composition via the Authentication Tests. In: de Alfaro, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2009. Lecture Notes in Computer Science, vol 5504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00596-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-00596-1_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00595-4
Online ISBN: 978-3-642-00596-1
eBook Packages: Computer ScienceComputer Science (R0)