Abstract
Proofs of security protocols typically employ simple abstractions of cryptographic operations, so that large parts of such proofs are independent of cryptographic details. The typical abstraction is the Dolev-Yao model, which treats cryptographic operations as a specific term algebra. However, there is no cryptographic semantics, i.e., no theorem that says what a proof with the Dolev-Yao abstraction implies for the real protocol, even if provably secure cryptographic primitives are used.
Recently we introduced an extension to the Dolev-Yao model for which such a cryptographic semantics exists, i.e., where security is preserved if the abstractions are instantiated with provably secure cryptographic primitives. Only asymmetric operations (digital signatures and public-key encryption) are considered so far. Here we extend this model to include a first symmetric primitive, message authentication, and prove that the extended model still has all desired properties. The proof is a combination of a probabilistic, imperfect bisimulation with cryptographic reductions and static information-flow analysis.
Considering symmetric primitives adds a major complication to the original model: we must deal with the exchange of secret keys, which might happen any time before or after the keys have been used for the first time. Without symmetric primitives only public keys need to be exchanged.
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., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. In: Proc. 4th ACM Conference on Computer and Communications Security, pp. 36–47 (1997)
Abadi, M., Jürjens, J.: Formal eavesdropping and its computational interpretation. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 82–94. Springer, Heidelberg (2001)
Abadi, M., Rogaway, P.: Reconciling two views of cryptography: The computational soundness of formal encryption. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 3–22. Springer, Heidelberg (2000)
Backes, M., Pfitzmann, B., Waidner, M.: Symmetric authentication within a simulatable cryptographic library. IACR Cryptology ePrint Archive 2003/145 (July 2003), http://eprint.iacr.org/
Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. IACR Cryptology ePrint Archive 2003/015 (January 2003), http://eprint.iacr.org/
Bellare, M., Canetti, R., Krawczyk, H.: Keying hash functions for message authentication. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol. 1109, pp. 1–15. Springer, Heidelberg (1996)
Canetti, R.: A unified framework for analyzing security of protocols. IACR Cryptology ePrint Archive 2000/067 (December 2001), http://eprint.iacr.org/
Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: Proc. 42nd IEEE Symposium on Foundations of Computer Science (FOCS), pp. 136–145 (2001)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
Goldwasser, S., Micali, S., Rivest, R.L.: A digital signature scheme secure against adaptive chosen-message attacks. SIAM Journal on Computing 17(2), 281–308 (1988)
Guttman, J.D., Thayer Fabrega, F.J., Zuck, L.: The faithfulness of abstract protocol analysis: Message authentication. In: Proc. 8th ACM Conference on Computer and Communications Security, pp. 186–195 (2001)
Hirt, M., Maurer, U.: Player simulation and general adversary structures in perfect multiparty computation. Journal of Cryptology 13(1), 31–60 (2000)
Kemmerer, R., Meadows, C., Millen, J.: Three systems for cryptographic protocol analysis. Journal of Cryptology 7(2), 79–130 (1994)
Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: Proc. 5th ACM Conference on Computer and Communications Security, pp. 112–121 (1998)
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)
Meadows, C.: Using narrowing in the analysis of key management protocols. In: Proc. 10th IEEE Symposium on Security & Privacy, pp. 138–147 (1989)
Millen, J.K.: The interrogator: A tool for cryptographic protocol security. In: Proc. 5th IEEE Symposium on Security & Privacy, pp. 134–141 (1984)
Paulson, L.: The inductive approach to verifying cryptographic protocols. Journal of Cryptology 6(1), 85–128 (1998)
Pfitzmann, B., Schunter, M., Waidner, M.: Cryptographic security of reactive systems. Presented at the DERA/RHUL Workshop on Secure Architectures and Information Flow, 1999, Electronic Notes in Theoretical Computer Science (ENTCS) (March 2000), http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/menu.htm
Pfitzmann, B., Waidner, M.: Composition and integrity preservation of secure reactive systems. In: Proc. 7th ACM Conference on Computer and Communications Security, pp. 245–254 (2000)
Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: Proc. 22nd IEEE Symposium on Security & Privacy, pp. 184–200 (2001)
Roscoe, A.W.: Modelling and verifying key-exchange protocols using CSP and FDR. In: Proc. 8th IEEE Computer Security Foundations Workshop (CSFW), pp. 98–107 (1995)
Schneider, S.: Security properties and CSP. In: Proc. 17th IEEE Symposium on Security & Privacy, pp. 174–187 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Backes, M., Pfitzmann, B., Waidner, M. (2003). Symmetric Authentication within a Simulatable Cryptographic Library. In: Snekkenes, E., Gollmann, D. (eds) Computer Security – ESORICS 2003. ESORICS 2003. Lecture Notes in Computer Science, vol 2808. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39650-5_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-39650-5_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20300-1
Online ISBN: 978-3-540-39650-5
eBook Packages: Springer Book Archive