Abstract
We present a general method to prove security properties of cryptographic protocols against active adversaries, when the messages exchanged by the honest parties are arbitrary expressions built using encryption and concatenation operations. The method allows to express security properties and carry out proofs using a simple logic based language, where messages are represented by syntactic expressions, and does not require dealing with probability distributions or asymptotic notation explicitly. Still, we show that the method is sound, meaning that logic statements can be naturally interpreted in the computational setting in such a way that if a statement holds true for any abstract (symbolic) execution of the protocol in the presence of a Dolev-Yao adversary, then its computational interpretation is also correct in the standard computational model where the adversary is an arbitrary probabilistic polynomial time program. This is the first paper providing a simple framework for translating security proofs from the logic setting to the standard computational setting for the case of powerful active adversaries that have total control of the communication network.
Research supported in part by NSF Grants CCR-0093029 and CCR-0313241
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., 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). Journal of Cryptology 15(2), 103–127 (2002)
Backes, M., Pfitzmann, B.: A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol. Available as Cryptology ePrint Archive, Report 2003/121
Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. Available as Cryptology ePrint Archive, Report 2003/015
Bellare, M., Boldyreva, A., Micali, S.: Public-key encryption in a multi-user setting: Security proofs and improvements. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 259–274. Springer, Heidelberg (2000)
Bellare, M., Pointcheval, D., Rogaway, P.: Authenticated key exchange secure against dictionary attacks. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, p. 139. Springer, Heidelberg (2000)
Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol. 773, pp. 232–249. Springer, Heidelberg (1994)
Bellare, M., Rogaway, P.: Provably secure session key distribution: the three party case. In: Proc. of 27th Anual Symposium on the Theory of Computing. ACM, New York (1995)
Canetti, R.: Universally composable security: A new paradigm for cryptographic protocols. In: Proceedings of FOCS 2001, pp. 136–145 (2001)
Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Transactions on Information Theory 29, 198–208 (1983)
Fabrega, F.J.T., Hertzog, J., Guttman, J.: Strand spaces: Proving security protocols correct. Journal of Computer Security 7(2/3), 191–230 (1999)
Gligor, V., Horvitz, D.O.: Weak Key Authenticity and the Computational Completeness of Formal Encryption. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 530–547. Springer, Heidelberg (2003)
Herzog, J.: Computational soundness of formal adversaries. Master Thesis
Herzog, J., Liskov, M., Micali, S.: Plaintext awareness via key registration. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 548–564. Springer, Heidelberg (2003)
Impagliazzo, R., Kapron, B.: Logics for reasoning about cryptographic constructions. In: STOC 2003, pp. 372–383 (2003)
Lincoln, P.D., Mitchell, J.C., Mitchell, M., Scedrov, A.: A probabilistic poly-time framework for protocol analysis. In: Computer and Communications Security - CCS 1998, San Francisco, California, USA, November 1998, pp. 112–121. ACM, New York (1998)
Lowe, G.: Breaking and fixing the Needham-Schröeder algorithm. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Micciancio, D., Warinschi, B.: Completeness theorems for the Abadi-Rogaway logic of encrypted expressions. Journal of Computer Security 12(1), 99–129 (2004)
Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6, 85–128 (1998)
Rackoff, C., Simon, D.R.: Non-interactive zero-knowledge proof of knowledge and chosen ciphertext attack. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 433–444. Springer, Heidelberg (1992)
Song, D.: An automatic checker for security protocol analysis. In: 12th IEEE Computer Security Foundations Workshop (June 1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Micciancio, D., Warinschi, B. (2004). Soundness of Formal Encryption in the Presence of Active Adversaries. In: Naor, M. (eds) Theory of Cryptography. TCC 2004. Lecture Notes in Computer Science, vol 2951. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24638-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-24638-1_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21000-9
Online ISBN: 978-3-540-24638-1
eBook Packages: Springer Book Archive