Hostname: page-component-745bb68f8f-hvd4g Total loading time: 0 Render date: 2025-01-24T09:32:49.699Z Has data issue: false hasContentIssue false
  • English
  • Français

The computational SLR: a logic for reasoning about computational indistinguishability

Published online by Cambridge University Press:  27 October 2010

YU ZHANG
YU ZHANG*
Affiliation:
State Key Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences, P.O. Box 8718, Beijing 100190, China and State Key Laboratory for Novel Software Technology, Nanjing University Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Computational indistinguishability is a notion in complexity-theoretic cryptography and is used to define many security criteria. However, in traditional cryptography, proving computational indistinguishability is usually informal and becomes error-prone when cryptographic constructions are complex. This paper presents a formal proof system based on an extension of Hofmann's SLR language, which can capture probabilistic polynomial-time computations through typing and is sufficient for expressing cryptographic constructions. In particular, we define rules that directly justify the computational indistinguishability between programs, and then prove that these rules are sound with respect to the set-theoretic semantics, and thus the standard definition of security. We also show that it is applicable in cryptography by verifying, in our proof system, Goldreich and Micali's construction of a pseudorandom generator, and the equivalence between next-bit unpredictability and pseudorandomness.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 20 , Special Issue 5: Theory and Applications of Models of Computation (TAMC 2008–2009) , October 2010 , pp. 951 - 975
Copyright
Copyright © Cambridge University Press 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Backes, M., Berg, M. and Unruh, D. (2008) A formal language for cryptographic pseudocode. In: 4th Workshop on Formal and Computational Cryptography (FCC 2008).Google Scholar
Barthe, G., Grégoire, B. and Zanella, S. (2009) Formal certification of code-based cryptographic proofs. In: 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'2009) 90–101.CrossRefGoogle Scholar
Bellantoni, S. and Cook, S. (1992) A new recursion-theoretic characterization of the polytime functions. Computational Complexity 2 97–110.CrossRefGoogle Scholar
Bellare, M. and Rogaway, P. (2004) Code-based game-playing proofs and the security of triple encryption. Cryptology ePrint Archive, Report 2004/331.Google Scholar
Blanchet, B. (2006) A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy (S&P'06) 140–154.CrossRefGoogle Scholar
Goldreich, O. (2001) The Foundations of Cryptography: Basic Tools, Cambridge University Press.CrossRefGoogle Scholar
Hofmann, M. (1998) A mixed modal/linear lambda calculus with applications to Bellantoni–Cook safe recursion. In: Proceedings of the International Workshop of Computer Science Logic (CSL'97). Springer-Verlag Lecture Notes in Computer Science 1414 275–294.CrossRefGoogle Scholar
Hofmann, M. (2000) Safe recursion with higher types and BCK-algebra. Annals of Pure and Applied Logic 104 (1–3)113–166.CrossRefGoogle Scholar
Impagliazzo, R. and Kapron, B. M. (2006) Logics for reasoning about cryptographic constructions. Journal of Computer and System Sciences 72 (2)286–320.CrossRefGoogle Scholar
Mitchell, J. C., Mitchell, M. and Scedrov, A. (1998) A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In: 39th Annual Symposium on Foundations of Computer Science (FOCS'98) 725–733.CrossRefGoogle Scholar
Mitchell, J. C., Ramanathan, A., Scedrov, A. and Teague, V. (2006) A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theoretical Computer Science 353 (1–3)118–164.Google Scholar
Moggi, E. (1991) Notions of computation and monads. Information and Computation 93 (1)55–92.CrossRefGoogle Scholar
Nowak, D. (2008) A framework for game-based security proofs. In: 9th International Conference of Information and Communications Security (ICICS 2007). Springer-Verlag Lecture Notes in Computer Science 4861 319–333.CrossRefGoogle Scholar
Nowak, D. and Zhang, Y. (2010) A calculus for game-based security proofs. In: Proceedings of 4th International Conference on Provable Security (ProvSec'2010). Springer-Verlag Lecture Notes in Computer Science 6402.Google Scholar
Ramsey, N. and Pfeffer, A. (2002) Stochastic lambda calculus and monads of probability distributions. In: 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'02) 154–165.CrossRefGoogle Scholar
Shoup, V. (2004) Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332.Google Scholar