Abstract
Automated tools such as model checkers and theorem provers for the analysis of security protocols typically abstract from cryptography by Dolev-Yao models, i.e., abstract term algebras replace the real cryptographic operations. Recently it was shown that in essence this approach is cryptographically sound for certain operations like signing and encryption. The strongest results show this in the sense of blackbox reactive simulatability (BRSIM)/UC with only small changes to both Dolev-Yao models and natural implementations. This notion essentially means the preservation of arbitrary security properties under active attacks in arbitrary protocol environments.
We show that it is impossible to extend the strong BRSIM/UC results to usual Dolev-Yao models of hash functions in the general case. These models treat hash functions as free operators of the term algebra. This result does not depend on any restriction of the real hash function; even probabilistic hashing is covered. In contrast, we show that these models are sound in the same strict sense in the random oracle model of cryptography. For the standard model of cryptography, we also discuss several conceivable restrictions and extensions to the Dolev-Yao models and classify them into possible and impossible cases in the strong BRSIM/UC sense.
Chapter PDF
Similar content being viewed by others
References
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.: A cryptographically sound dolev-yao style security proof of the otway-rees protocol. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 89–108. Springer, Heidelberg (2004)
Backes, M., Dürmuth, M.: A cryptographically sound Dolev-Yao style security proof of an electronic payment system. In: Proc. 18th IEEE CSFW, pp. 78–93 (2005)
Backes, M., Pfitzmann, B.: A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol. Journal on Selected Areas in Communications 22(10), 2075–2086 (2004)
Backes, M., Pfitzmann, B.: Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In: Proc. 17th IEEE CSFW, pp. 204–218 (2004)
Backes, M., Pfitzmann, B.: Limits of the cryptographic realization of dolev-yao-style XOR. In: di Vimercati, S.d.C., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 178–196. Springer, Heidelberg (2005)
Backes, M., Pfitzmann, B., Waidner, M.: A composable cryptographic library with nested operations. In: Proc. 10th ACM CCS, pp. 220–230 (2003)
Backes, M., Pfitzmann, B., Waidner, M.: Symmetric authentication within a simulatable cryptographic library. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 271–290. Springer, Heidelberg (2003)
Backes, M., Pfitzmann, B., Waidner, M.: Limits of the Reactive Simulatability/UC of Dolev-Yao models with hashes. IACR Cryptology ePrint Archive 2006/068 (February 2006)
Basin, D., Mödersheim, S., Viganò, L.: OFMC: A symbolic model checker for security protocols. Intern. Journal of Information Security (2004)
Bellare, M., Rogaway, P.: Random oracles are practical: A paradigm for designing efficient protocols. In: Proc. 1st ACM CCS, pp. 62–73 (1993)
Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proc. 14th IEEE CSFW, pp. 82–96 (2001)
Blanchet, B.: A computationally sound mechanized prover for security protocols. In: Proc. 27th IEEE Symp. on Security & Privacy, pp. 140–154 (2006)
Canetti, R.: Towards realizing random oracles: Hash functions that hide all partial information. In: Kaliski Jr., B.S. (ed.) CRYPTO 1997. LNCS, vol. 1294, pp. 455–469. Springer, Heidelberg (1997)
Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: Proc. 42nd IEEE FOCS, pp. 136–145 (2001)
Canetti, R., Fischlin, M.: Universally composable commitments. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol. 2139, pp. 19–40. Springer, Heidelberg (2001)
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)
Canetti, R., Krawczyk, H.: Universally composable notions of key exchange and secure channels. In: Knudsen, L.R. (ed.) EUROCRYPT 2002. LNCS, vol. 2332, pp. 337–351. Springer, Heidelberg (2002)
Canetti, R., Micciancio, D., Reingold, O.: Perfectly one-way probabilistic hash functions. In: Proc. 30th ACM STOC, pp. 131–140 (1998)
Datta, A., Derek, A., Mitchell, J.C., Ramanathan, A., Scedrov, A.: Games and the impossibility of realizable ideal functionality. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 360–379. Springer, Heidelberg (2006)
Datta, A., Derek, A., Mitchell, J.C., Shmatikov, V., Turuani, M.: Probabilistic polynomial-time semantics for a protocol security logic. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 16–29. Springer, Heidelberg (2005)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
Garcia, F.D., van Rossum, P.: Sound computational interpretation of formal hashes. IACR Cryptology ePrint Archive 2006/014 (January 2006)
Hofheinz, D., Müller-Quade, J.: Universally composable commitments using random oracles. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 58–76. Springer, Heidelberg (2004)
Impagliazzo, R., Kapron, B.M.: Logics for reasoning about cryptographic constructions. In: Proc. 44th IEEE FOCS, pp. 372–381 (2003)
Laud, P.: Semantics and program analysis of computationally secure information flow. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 77–91. Springer, Heidelberg (2001)
Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: Proc. 25th IEEE Symp. on Security & Privacy, pp. 71–85 (2004)
Laud, P.: Secrecy types for a simulatable cryptographic library. In: Proc. 12th ACM CCS, pp. 26–35 (2005)
Merritt, M.: Cryptographic Protocols. PhD thesis, Georgia Institute of Technology (1983)
Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 133–151. Springer, Heidelberg (2004)
Mitchell, J., Mitchell, M., Scedrov, A.: A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In: Proc. 39th FOCS, pp. 725–733 (1998)
Mitchell, J., Mitchell, M., Scedrov, A., Teague, V.: A probabilistic polynominal-time process calculus for analysis of cryptographic protocols. ENTCS 47, 1–31 (2001)
Paulson, L.: The inductive approach to verifying cryptographic protocols. Journal of Cryptology 6(1), 85–128 (1998)
Pfitzmann, B., Waidner, M.: Composition and integrity preservation of secure reactive systems. In: Proc. 7th ACM CCS, 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 Symp. on S & P, pp. 184–200 (2001)
Sprenger, C., Backes, M., Basin, D., Pfitzmann, B., Waidner, M.: Cryptographically sound theorem proving. In: Proc. 19th IEEE CSFW (to appear, 2006)
Yao, A.C.: Theory and applications of trapdoor functions. In: Proc. 23rd FOCS, pp. 80–91 (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Backes, M., Pfitzmann, B., Waidner, M. (2006). Limits of the BRSIM/UC Soundness of Dolev-Yao Models with Hashes. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds) Computer Security – ESORICS 2006. ESORICS 2006. Lecture Notes in Computer Science, vol 4189. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11863908_25
Download citation
DOI: https://doi.org/10.1007/11863908_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44601-9
Online ISBN: 978-3-540-44605-7
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
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.