iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://doi.org/10.1007/978-981-97-8943-6_12
On Computational Indistinguishability and Logical Relations | SpringerLink
Skip to main content
Springer Nature Link
Log in

On Computational Indistinguishability and Logical Relations

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 15194))

Included in the following conference series:

  • 52 Accesses

Abstract

A \(\lambda \)-calculus is introduced in which all programs can be evaluated in probabilistic polynomial time and in which there is sufficient structure to represent sequential cryptographic constructions and adversaries for them, even when the latter are oracle-based. A notion of observational equivalence capturing computational indistinguishability and a class of approximate logical relations are then presented, showing that the latter represent a sound proof technique for the former. The work concludes with the presentation of an example of a security proof in which the encryption scheme induced by a pseudorandom function is proven secure against active adversaries in a purely equational style.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 49.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 59.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Abadi, M.: Security protocols: principles and calculi. In: Aldini, A., Gorrieri, R. (eds.) Foundations of Security Analysis and Design IV, pp. 1–23 (2006). https://doi.org/10.1007/978-3-540-74810-6_1

  2. Abramsky, S.: The lazy lambda calculus. In: Research Topics in Functional Programming, pp. 65-116. Addison-Wesley Longman Publishing Co., Inc. (1990)

    Google Scholar 

  3. Accattoli, B., Dal Lago, U.: (Leftmost-outermost) beta reduction is invariant, indeed. Log. Methods Comput. Sci. 12(1) (2016). https://doi.org/10.2168/LMCS-12(1:4)2016

  4. Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Katsumata, S.Y., Sato, T.: Higher-order probabilistic adversarial computations: categorical semantics and program logics. In: Proceedings of the ICFP 2021, pp. 1–30. ACM (2021). https://doi.org/10.1145/3473598

  5. Aguirre, A., Birkedal, L.: Step-indexed logical relations for countable nondeterminism and probabilistic choice. In: Proceedings of POPL 2023, vol. 7, pp. 33–60. ACM (2023). https://doi.org/10.1145/3571195

  6. Baelde, D., Jacomme, C.: The squirrel prover and its logic. ACM SIGLOG News 11(2), 62–83 (2024). https://doi.org/10.1145/3665453.3665461

    Article  Google Scholar 

  7. Balan, A., Kurz, A., Velebil, J.: Extending set functors to generalised metric spaces. Log. Methods Comput. Sci. 15(1) (2019). https://doi.org/10.23638/LMCS-15(1:5)2019

  8. Baldan, P., Bonchi, F., Kerstan, H., König, B.: Coalgebraic behavioral metrics. Log. Methods Comput. Sci. 14(3) (2018). https://doi.org/10.23638/LMCS-14(3:20)2018

  9. Bana, G., Comon-Lundh, H.: A computationally complete symbolic attacker for equivalence properties. In: Proceedings of the CCS 2014, pp. 609–620 (2014). https://doi.org/10.1145/2660267.2660276

  10. Bellare, M.: A note on negligible functions. J. Cryptol. 15(4), 271–284 (2002). https://doi.org/10.1007/s00145-002-0116-x

    Article  MathSciNet  Google Scholar 

  11. Bizjak, A., Birkedal, L.: Step-indexed logical relations for probability. In: Proceedings of FoSSaCS 2015, pp. 279–294. Springer (2015). https://doi.org/10.1007/978-3-662-46678-0_18

  12. van Breugel, F.: The metric monad for probabilistic nondeterminism. Draft available at http://www.cse.yorku.ca/franck/research/drafts/monad.pdf (2005)

  13. Canetti, R., Stoughton, A., Varia, M.: EasyUC: using EasyCrypt to mechanize proofs of universally composable security. In: Proceedings of the CSF 2019, pp. 167–183. IEEE (2019). https://doi.org/10.1109/CSF.2019.00019

  14. Dal Lago, U., Galal, Z., Giusti, G.: On Computational Indistinguishability and Logical Relations (2024). http://arxiv.org/abs/2408.17340

  15. Dal Lago, U., Gavazzo, F.: A relational theory of effects and coeffects. In: Proceedings of the POPL 2022, vol. 6, pp. 1–28. ACM (2022). https://doi.org/10.1145/3498692

  16. Dal Lago, U., Giusti, G.: On session typing, probabilistic polynomial time, and cryptographic experiments. In: Proceedings of the CONCUR 2022, vol. 243, pp. 37:1–37:18 (2022). https://doi.org/10.4230/LIPICS.CONCUR.2022.37

  17. Dal Lago, U., Martini, S.: On constructor rewrite systems and the lambda calculus. Log. Methods Comput. Sci. (2012). https://doi.org/10.1007/978-3-642-02930-1_14

    Article  MathSciNet  Google Scholar 

  18. Dal Lago, U., Petit, B.: Linear dependent types in a call-by-value scenario. In: Proceedings of the PPDP 2012, pp. 115–126. ACM (2012). https://doi.org/10.1145/2370776.2370792

  19. Dal Lago, U., Zuppiroli, S., Gabbrielli, M.: Probabilistic recursion theory and implicit computational complexity. Sci. Ann. Comput. Sci. 177–216 (2014). https://doi.org/10.7561/SACS.2014.2.177

  20. Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–207 (1983). https://doi.org/10.1109/TIT.1983.1056650

    Article  MathSciNet  Google Scholar 

  21. Ehrhard, T., Tasson, C.: Probabilistic call by push value. Log. Methods Comput. Sci. 15(1) (2019). https://doi.org/10.23638/LMCS-15(1:3)2019

  22. Fiore, M., Abadi, M.: Computing symbolic models for verifying cryptographic protocols. In: Proceedings of the CSFW 2001, pp. 160–173. IEEE (2001). https://doi.org/10.1109/CSFW.2001.930144

  23. Gavazzo, F.: Quantitative behavioural reasoning for higher-order effectful programs: applicative distances. In: Proceedings of the LICS 2018, pp. 452–461. ACM (2018). https://doi.org/10.1145/3209108.3209149

  24. Gibbs, A.L., Su, F.E.: On choosing and bounding probability metrics. Int. Stat. Rev. 70(3), 419–435 (2002). https://doi.org/10.2307/1403865

    Article  Google Scholar 

  25. Gifford, D.K., Lucassen, J.M.: Integrating functional and imperative programming. In: Proceedings of the 1986 ACM Conference on LISP and Functional Programming, pp. 28–38. ACM (1986). https://doi.org/10.1145/319838.319848

  26. Girard, J.Y., Scedrov, A., Scott, P.J.: Bounded linear logic: a modular approach to polynomial-time computability. Theoret. Comput. Sci. 97(1), 1–66 (1992). https://doi.org/10.1016/0304-3975(92)90386-T

    Article  MathSciNet  Google Scholar 

  27. Goldreich, O.: Foundations of Cryptography. Vol. 1: Basic Tools. Cambridge University Press, Cambridge (2007)

    Google Scholar 

  28. Goldwasser, S., Micali, S.: Probabilistic encryption. J. Comput. Syst. Sci. 28(2), 270–299 (1984). https://doi.org/10.1016/0022-0000(84)90070-9

    Article  MathSciNet  Google Scholar 

  29. Gordon, A.D.: Operational equivalences for untyped and polymorphic object calculi. In: Higher-Order Operational Techniques in Semantics, Publications of the Newton Institute, pp. 9–54. Cambridge University Press (1998)

    Google Scholar 

  30. Goubault-Larrecq, J., Lasota, S., Nowak, D.: Logical relations for monadic types. Math. Struct. Comput. Sci. 1169–1217 (2008). https://doi.org/10.1007/3-540-45793-3_37

  31. Goubault-Larrecq, J., Lasota, S., Nowak, D., Zhang, Y.: Complete lax logical relations for cryptographic lambda-calculi. In: Proceedings of the CSL 2004, pp. 400–414. Springer (2004).https://doi.org/10.1007/978-3-540-30124-0_31

  32. Hofmann, D., Seal, G.J., Tholen, W.: Monoidal Topology: A Categorical Approach to Order, Metric, and Topology. Cambridge University Press (2014)

    Google Scholar 

  33. Hyland, M., Plotkin, G., Power, J.: Combining effects: sum and tensor. Theoret. Comput. Sci. 357(1), 70–99 (2006). https://doi.org/10.1016/j.tcs.2006.03.013

    Article  MathSciNet  Google Scholar 

  34. Impagliazzo, R., Kapron, B.M.: Logics for reasoning about cryptographic constructions. J. Comput. Syst. Sci. 72(2), 286–320 (2006). https://doi.org/10.1016/j.jcss.2005.06.008

    Article  MathSciNet  Google Scholar 

  35. Kantorovich, L.V.: On the translocation of masses. J. Math. Sci. 133(4), 1381–1382 (2006). https://doi.org/10.1007/s10958-006-0049-2

    Article  MathSciNet  Google Scholar 

  36. Katz, J., Lindell, Y.: Introduction to Modern Cryptography. CRC Press (2020)

    Google Scholar 

  37. Lassen, S.B.: Relational reasoning about contexts. In: Higher-Order Operational Techniques in Semantics, Publications of the Newton Institute, vol. 91, pp. 91–136. Cambridge University Press (1998)

    Google Scholar 

  38. Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284–304 (2009). https://doi.org/10.1016/j.ic.2007.12.004

    Article  MathSciNet  Google Scholar 

  39. Levy, P.B.: Call-by-Push-Value: A Functional/Imperative Synthesis, vol. 2. Springer Science & Business Media (2012)

    Google Scholar 

  40. Mardare, R., Panangaden, P., Plotkin, G.: Quantitative algebraic reasoning. In: Proceedings of the LICS 2016, pp. 700–709. ACM (2016). https://doi.org/10.1145/2933575.2934518

  41. Mitchell, J., Mitchell, M., Scedrov, A.: A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In: Proceedings of the SFCS 1998, pp. 725–733. IEEE (1998). https://doi.org/10.1109/SFCS.1998.743523

  42. Mitchell, J.C., Ramanathan, A., Scedrov, A., Teague, V.: A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theoret. Comput. Sci. 353(1–3) (2006). https://doi.org/10.1016/j.tcs.2005.10.044

  43. Mitchell, J.C.: Multiset rewriting and security protocol analysis. In: Proceedings of the RTA 2002, pp. 19–22. Springer (2002). https://doi.org/10.1007/3-540-45610-4_2

  44. Mitchell, J.C., Scedrov, A.: Notes on sconing and relators. In: Proceedings of the CSL 1992, pp. 352–378. Springer (1992). https://doi.org/10.1007/3-540-56992-8_21

  45. Nowak, D., Zhang, Y.: A calculus for game-based security proofs. In: Proceedings of the ProvSec 2010. Springer (2010). https://doi.org/10.1007/978-3-642-16280-0_3

  46. Reed, J., Pierce, B.C.: Distance makes the types grow stronger: a calculus for differential privacy. In: Proceedings of the ICFP 2010, pp. 157–168. ACM (2010). https://doi.org/10.1145/1863543.1863568

  47. Rosenthal, K.I.: Quantales and Their Applications. Wiley (1990)

    Google Scholar 

  48. Sangiorgi, D., Rutten, J.: Advanced Topics in Bisimulation and Coinduction. Cambridge University Press (2011)

    Google Scholar 

  49. Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. IACR Cryptol. ePrint Arch., p. 332 (2004). http://eprint.iacr.org/2004/332

  50. Statman, R.: Logical relations and the typed \(\lambda \)-calculus. Inf. Control 65(2–3), 85–97 (1985). https://doi.org/10.1016/S0019-9958(85)80001-2

  51. Tait, W.W.: Intensional interpretations of functionals of finite type I. J. Symbol. Log. 32(2), 198–212 (1967). https://doi.org/10.2307/2271658

    Article  MathSciNet  Google Scholar 

  52. Wild, P., Schröder, L.: Characteristic logics for behavioural hemimetrics via fuzzy lax extensions. Log. Methods Comput. Sci. (2022). https://doi.org/10.46298/lmcs-18(2:19)2022

Download references

Acknowledgements

The first two authors are partially supported by the MUR FARE project CAFFEINE, and by the ANR PRC project PPS (ANR-19-CE48-0014). The third author is partially supported by Fondation CFM.

Author information

Authors and Affiliations

  1. University of Bologna, Bologna, Italy

    Ugo Dal Lago & Zeinab Galal

  2. INRIA Sophia Antipolis, Valbonne, France

    Ugo Dal Lago & Zeinab Galal

  3. ENS Lyon, Lyon, France

    Giulia Giusti

Authors
  1. Ugo Dal Lago
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zeinab Galal
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Giulia Giusti
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zeinab Galal .

Editor information

Editors and Affiliations

  1. Tohoku University, Sendai, Miyagi, Japan

    Oleg Kiselyov

Rights and permissions

Reprints and permissions

Copyright information

© 2025 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lago, U.D., Galal, Z., Giusti, G. (2025). On Computational Indistinguishability and Logical Relations. In: Kiselyov, O. (eds) Programming Languages and Systems. APLAS 2024. Lecture Notes in Computer Science, vol 15194. Springer, Singapore. https://doi.org/10.1007/978-981-97-8943-6_12

Download citation

  • DOI: https://doi.org/10.1007/978-981-97-8943-6_12

  • Published:

  • Publisher Name: Springer, Singapore

  • Print ISBN: 978-981-97-8942-9

  • Online ISBN: 978-981-97-8943-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation