Veronique Cortier
ABSTRACT
Computational soundness results show that under certain conditions it is possible to conclude computational security whenever symbolic security holds. Unfortunately, each soundness result is usually established for some set of cryptographic primitives and extending the result to encompass new primitives typically requires redoing most of the work. In this paper we suggest a way of getting around this problem. We propose a notion of computational soundness that we term deduction soundness. As for other soundness notions, our definition captures the idea that a computational adversary does not have any more power than a symbolic adversary. However, a key aspect of deduction soundness is that it considers, intrinsically, the use of the primitives in the presence of functions specified by the adversary. As a consequence, the resulting notion is amenable to modular extensions. We prove that a deduction sound implementation of some arbitrary primitives can be extended to include asymmetric encryption and public data-structures (e.g. pairings or list), without repeating the original proof effort. Furthermore, our notion of soundness concerns cryptographic primitives in a way that is independent of any protocol specification language. Nonetheless, we show that deduction soundness leads to computational soundness for languages (or protocols) that satisfy a so called commutation property.
- M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology, 15(2):103--127, 2002.Google Scholar
Digital Library
- A. Armando, R. Carbone, L. Compagna, J. Cuellar, and L. T. Abad. Formal analysis of saml 2.0 web browser single sign-on: Breaking the saml-based single sign-on for google apps. In Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering (FMSE 2008), pages 1--10, 2008. Google ScholarDigital Library
- M. Backes, D. Hofheinz, and D. Unruh. Cosp: A general framework for computational soundness proofs. In ACM CCS 2009, pages 66--78, November 2009. Preprint on IACR ePrint 2009/080. Google ScholarDigital Library
- M. Backes and B. Pfitzmann. Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In Proc. 17th IEEE Computer Science Foundations Workshop (CSFW'04), pages 204--218, 2004. Google ScholarDigital Library
- M. Backes, B. Pfitzmann, and M. Waidner. A composable cryptographic library with nested operations. In Proc. 10th ACM Conference on Computer and Communications Security (CCS'03), 2003. Google ScholarDigital Library
- M. Backes and D. Unruh. Computational soundness of symbolic zero-knowledge proofs against active attackers. In Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF'08), pages 255--269, Pittsburgh, PA, USA, June 2008. IEEE Computer Society Press. Google ScholarDigital Library
- R. Canetti. Universally composable signature, certification, and authentication. In Proc. 17th IEEE Computer Security Foundations Workshop (CSFW'04), pages 219--235, 2004. Google ScholarDigital Library
- R. Canetti and J. Herzog. Universally composable symbolic analysis of mutual authentication and key-exchange protocols (extended abstract). In Proc. 3rd Theory of Cryptography Conference (TCC'06), volume 3876 of LNCS, pages 380--403. Springer, 2006. Google ScholarDigital Library
- H. Comon-Lundh and V. Cortier. Computational soundness of observational equivalence. In Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS'08), Alexandria, Virginia, USA, Oct. 2008. ACM Press. Google ScholarDigital Library
- H. Comon-Lundh and V. Cortier. How to prove security of communication protocols\u n A discussion on the soundness of formal models w.r.t. computational ones. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011), volume 9 of Leibniz International Proceedings in Informatics (LIPIcs), pages 29--44, 2011.Google Scholar
- V. Cortier, S. Kremer, R. Küsters, and B. Warinschi. Computationally sound symbolic secrecy in the presence of hash functions. In Proceedings of the 26th Conference on Fundations of Software Technology and Theoretical Computer Science (FSTTCS'06), volume 4337 of LNCS, pages 176--187, Kolkata, India, 2006. Springer. Google ScholarDigital Library
- V. Cortier, S. Kremer, and B. Warinschi. A survey of symbolic methods in computational analysis of cryptographic systems. J. Autom. Reasoning, 46(3--4):225--259, 2011. 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, Edinburgh, UK, 2005. Springer. Google ScholarDigital Library
- D. Galindo, F. D. Garcia, and P. van Rossum. Computational soundness of non-malleable commitments. In Proc. 4th Information Security Practice and Experience Conference (ISPEC'08), LNCS, 2008. Google ScholarDigital Library
- J. Herzog. A computational interpretation of Dolev-Yao adversaries. Theoretical Computer Science, 340:57--81, June 2005. Google ScholarDigital Library
- 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
- R. Janvier, Y. Lakhnech, and L. Mazaré. Computational soundness of symbolic analysis for protocols using hash functions. In Proceedings of the Workshop on Information and Computer Security (ICS'06), Electronic Notes in Theoretical Computer Science, Timisoara, Romania, Sept. 2006. Elsevier Science Publishers.Google Scholar
- R. Küsters and M. Tuengerthal. Computational Soundness for Key Exchange Protocols with Symmetric Encryption. In E. Al-Shaer, S. Jha, and A. D. Keromytis, editors, Proceedings of the 16th ACM Conference on Computer and Communications Security (CCS 2009), pages 91--100. ACM Press, 2009. Google ScholarDigital Library
- G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96), volume 1055 of LNCS, pages 147--166. Springer-Verlag, March 1996. Google ScholarDigital Library
- D. Micciancio and B. Warinschi. Soundness of formal encryption in the presence of active adversaries. In Proc. 1st Theory of Cryptography Conference (TCC'04), volume 2951 of LNCS, pages 133--151. Springer, 2004.Google ScholarCross Ref
Index Terms
- A composable computational soundness notion
Recommendations
Deduction soundness: prove one, get five for free
CCS '13: Proceedings of the 2013 ACM SIGSAC conference on Computer & communications securityMost computational soundness theorems deal with a limited number of primitives, thereby limiting their applicability. The notion of deduction soundness of Cortier and Warinschi (CCS'11) aims to facilitate soundness theorems for richer frameworks via ...
Computational Soundness of a Call by Name Calculus of Recursively-scoped Records
The paper presents a calculus of recursively-scoped records: a two-level calculus with a traditional call-by-name @l-calculus at a lower level and unordered collections of labeled @l-calculus terms at a higher level. Terms in records may reference each ...
Computational soundness, co-induction, and encryption cycles
EUROCRYPT'10: Proceedings of the 29th Annual international conference on Theory and Applications of Cryptographic TechniquesWe analyze the relation between induction, co-induction and the presence of encryption cycles in the context of computationally sound symbolic equivalence of cryptographic expressions. Our main finding is that the use of co-induction in the symbolic ...
Comments