Hubert Comon-Lundh
ABSTRACT
Many security properties are naturally expressed as indistinguishability between two versions of a protocol. In this paper, we show that computational proofs of indistinguishability can be considerably simplified, for a class of processes that covers most existing protocols. More precisely, we show a soundness theorem, following the line of research launched by Abadi and Rogaway in 2000: computational indistinguishability in presence of an active attacker is implied by the observational equivalence of the corresponding symbolic processes. We prove our result for symmetric encryption, but the same techniques can be applied to other security primitives such as signatures and public-key encryption. The proof requires the introduction of new concepts, which are general and can be reused in other settings.
- M. Abadi, M. Baudet, and B. Warinschi. Guessing attacks and the computational soundness of static equivalence. In Foundations of Software Science and Computation Structure (FoSSaCS'06), volume 3921 of LNCS, pages 398--412, 2006.Google Scholar
Digital Library
- M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In Principles of Programming Languages (POPL'01), pages 104--115, 2001. Google ScholarDigital Library
- M. Abadi and J. Jürgens. Formal eavesdropping and its computational interpretation. In Theoretical Aspects of Computer Software, LNCS 2215, 2001. Google ScholarDigital Library
- M. Abadi and P. Rogaway. Reconciling two views of cryptography: the computational soundness of formal encryption. J. Cryptology, 2007.Google Scholar
- M. Abdalla and B. Warinschi. On the minimal assumptions of group signature schemes. In 6th International Conference on Information and Communication Security, pages 1--13, 2004.Google ScholarCross Ref
- P. Adao and C. Fournet. Cryptographically sound implementations for communicating processes. In International Colloquium on Algorithms, Languages and Programming (ICALP'06), 2006.Google ScholarDigital Library
- M. Backes, M. Dürmuth, and R. Küsters. On simulatability soundness and mapping soundness of symbolic cryptography. In Proc. of 27th FSTTCS, volume 4855 of LNCS, 2007.Google ScholarDigital Library
- M. Backes and B. Pfitzmann. Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In Computer Security Foundations Workshop (CSFW'04), 2004. Google ScholarDigital Library
- M. Backes and B. Pfitzmann. Relating cryptographic und symbolic key secrecy. In Symp. on Security and Privacy (SSP'05), pages 171--182, 2005. Google ScholarDigital Library
- M. Backes, B. Pfitzmann, and M. Waidner. A composable cryptographic library with nested operations. In 10th ACM Concerence on Computer and Communications Security (CCS'03), 2003. Google ScholarDigital Library
- M. Backes, B. Pfitzmann, and M. Waidner. The reactive simulatability (RSIM) framework for asynchronous systems. Information and Computation, 205(12):1685--1720, 2007. Google ScholarDigital Library
- M. Baudet, V. Cortier, and S. Kremer. Computationally sound implementations of equational theories against passive adversaries. In Proc. ICALP'05, volume 3580 of LNCS, 2005.Google ScholarDigital Library
- M. Bellare and C. Namprempre. Authenticated encryption: relations among notions and analysis of the generic composition paradigm. In Advances in Cryptology (ASIACRYPT 2000), volume 1976 of LNCS, pages 531--545, 2000. Google ScholarDigital Library
- B. Blanchet. An efficient cryptographic protocol verifier based on Prolog rules. In Computer Security Foundations Workshop (CSFW'01), 2001. Google ScholarDigital Library
- B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming, 75(1):3--51, 2008.Google ScholarCross Ref
- M. Burrows, M. Abadi, and R. Needham. A logic of authentication. Technical Report 39, Digital Systems Research Center, February 1989.Google Scholar
- R. Canetti. Universal composable security: a new paradigm for cryptographic protocols. In Symposium on Foundations of Computer Science, 2001. Google ScholarDigital Library
- R. Canetti and J. Herzog. Universally composable symbolic analysis of cryptographic protocols. In Theory of Cryptography Conference (TCC'06), 2006.Google ScholarDigital Library
- R. Canetti and T. Rabin. Universal composition with joint state. Cryptology ePrint Archive, report 2002/47, Nov. 2003.Google Scholar
- H. Comon-Lundh and V. Cortier. Computational soundness of observational equivalence. Research Report 6508, INRIA, https://hal.inria.fr/inria-00274158, Apr. 2008.Google Scholar
- V. Cortier, S. Kremer, R. Küsters, and B. Warinschi. Computationally sound symbolic secrecy in the presence of hash functions. In Proc. FSTTCS, volume 4337 of LNCS, pages 176--187, 2006.Google ScholarDigital Library
- V. Cortier and B. Warinschi. Computationally sound, automated proofs for security protocols. In European Symposium on Programming (ESOP'05), volume 3444 of LNCS, pages 157--171, 2005.Google ScholarDigital Library
- S. Delaune, S. Kremer, and M. D. Ryan. Coercion-resistance and receipt-freeness in electronic voting. In Computer Security Foundations Workshop (CSFW'06), pages 28--39, 2006. Google ScholarDigital Library
- S. Delaune, S. Kremer, and M. D. Ryan. Symbolic bisimulation for the applied pi-calculus. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07), volume 4855 of LNCS, pages 133--145, 2007.Google ScholarDigital Library
- H. Hüttel. Deciding framed bisimilarity. In Proc. INFINITY'02, 2002.Google ScholarCross Ref
- R. Janvier, Y. Lakhnech, and L. Mazaré. Completing the picture: Soundness of formal encryption in the presence of active adversaries. In European Symposium on Programming (ESOP'05), volume 3444 of LNCS, pages 172--185. Springer, 2005.Google ScholarDigital Library
- A. Juels, M. Luby, and R. Ostrovsky. Security of blind digital signatures. In advances in cryptology, (CRYPTO-97), volume 1294 of LNCS, pages 150--164, 1997. Google ScholarDigital Library
- S. Kremer and L. Mazaré. Adaptive soundness of static equivalence. In European Symposium on Research in Computer Security (ESORICS'07), volume 4734 of LNCS, pages 610--625, 2007.Google ScholarCross Ref
- R. Küsters and M. Tuengerthal. Joint state theorems for public-key encryption and digital signature functionalities with local computations. In Computer Security Foundations (CSF'08), 2008. Google ScholarDigital Library
- P. Laud. Symmetric encryption in automatic analyses for confidentiality against active adversaries. In Symp. on Security and Privacy (SSP'04), pages 71--85, 2004.Google Scholar
- D. Micciancio and B. Warinschi. Completeness theorems for the Abadi-Rogaway language of encrypted expressions. Journal of Computer Security, 2004. Google ScholarDigital Library
- D. Micciancio and B. Warinschi. Soundness of formal encryption in presence of an active attacker. In Theory of Cryptography Conference (TCC'04), volume 2951 of LNCS, 2004.Google ScholarCross Ref
- J. Mitchell, A. Ramanathan, and V. Teague. A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theoretical Comput. Sci., 353:118--164, 2006. Google ScholarDigital Library
Index Terms
- Computational soundness of observational equivalence
Recommendations
The security of a strong proxy signature scheme with proxy signer privacy protection
In 1996, Mambo et al. first introduced the concept of a proxy signature scheme, and discussed the delegation of the signing capability to a proxy signer. In 2001, Lee et al. constructed a strong non-designated proxy signature scheme. In 2002, Shum and ...
A new signature scheme without random oracles
Digital signature is commonly used for authentication of a user or data. In order to ensure the security of a signature scheme, it is important to design a signature scheme with a security proof. In 1999, Gennaro et al. and Cramer et al. respectively ...
A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol
We present a cryptographically sound security proof of the well-known Needham-Schroeder-Lowe public-key protocol for entity authentication. This protocol was previously only proved over unfounded abstractions from cryptography. We show that it is secure ...
Comments