Document Open Access Logo

On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments

Authors Ugo Dal Lago , Giulia Giusti

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2022.37.pdf
  • Filesize: 0.75 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
  • Theory of computation → Program semantics
  • Security and privacy → Mathematical foundations of cryptography
Keywords
  • Session Types
  • Probabilistic Computation
  • Bounded Linear Logic
  • Cryptographic Experiments

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

A system of session types is introduced as induced by a Curry Howard correspondence applied to bounded linear logic, suitably extended with probabilistic choice operators and ground types. The resulting system satisfies some expected properties, like subject reduction and progress, but also unexpected ones, like a polynomial bound on the time needed to reduce processes. This makes the system suitable for modelling experiments and proofs from the so-called computational model of cryptography.

Cite As Get BibTex

Ugo Dal Lago and Giulia Giusti. On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 37:1-37:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CONCUR.2022.37

Author Details

Ugo Dal Lago
  • University of Bologna, Italy
  • INRIA Sophia Antipolis, France
Giulia Giusti
  • University of Bologna, Italy

Funding

The authors are partially supported by the ERC CoG "DIAPASoN", GA 818616.

Acknowledgements

The authors would like to thank the anonymous referees for the many insightful comments.

References

  1. Martín Abadi, Ricardo Corin, and Cédric Fournet. Computational secrecy by typing for the pi calculus. In Proc. of APLAS 2006, volume 4279 of LNCS, pages 253-269. Springer, 2006. URL: https://doi.org/10.1007/11924661_16.
  2. Martín Abadi and Cédric Fournet. Mobile values, new names, and secure communication. In Proc. of POPL 2001, pages 104-115. ACM, 2001. URL: https://doi.org/10.1145/360204.360213.
  3. Martín Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus. Inf. Comput., 148(1):1-70, 1999. URL: https://doi.org/10.1006/inco.1998.2740.
  4. Bogdan Aman and Gabriel Ciobanu. Probabilities in session types. In Proc. of FROM 2019, volume 303 of EPTCS, pages 92-106, 2019. URL: https://doi.org/10.4204/EPTCS.303.7.
  5. Michael Backes, Esfandiar Mohammadi, and Tim Ruffing. Computational soundness results for proverif - bridging the gap from trace properties to uniformity. In Proc. of POST 2014, volume 8414 of LNCS, pages 42-62. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54792-8_3.
  6. Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, and Pierre-Yves Strub. Mechanized proofs of adversarial complexity and application to universal composability. In Proc. of CCS 2021, pages 2541-2563. ACM, 2021. URL: https://doi.org/10.1145/3460120.3484548.
  7. Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, and Pierre-Yves Strub. Relational reasoning via probabilistic coupling. In Proc. of LPAR 2015, volume 9450 of LNCS, pages 387-401. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_27.
  8. Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella Béguelin. Probabilistic relational verification for cryptographic implementations. In Proc. of POPL 2014, pages 193-206. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535847.
  9. Massimo Bartoletti, Ilaria Castellani, Pierre-Malo Deniélou, Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Jovanka Pantovic, Jorge A. Pérez, Peter Thiemann, Bernardo Toninho, and Hugo Torres Vieira. Combining behavioural types with security analysis. J. Log. Algebraic Methods Program., 84(6):763-780, 2015. URL: https://doi.org/10.1016/j.jlamp.2015.09.003.
  10. Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida. Monitoring networks through multiparty session types. Theor. Comput. Sci., 669:33-58, 2017. URL: https://doi.org/10.1016/j.tcs.2017.02.009.
  11. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In Proc. of CONCUR 2010, pages 222-236. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_16.
  12. Ran Canetti. Universally composable security: A new paradigm for cryptographic protocols. In Proc. of FOCS 2001, pages 136-145. IEEE, 2001. URL: https://doi.org/10.1109/SFCS.2001.959888.
  13. Ran Canetti. Universally composable security. J. ACM, 67(5):28:1-28:94, 2020. URL: https://doi.org/10.1145/3402457.
  14. Ran Canetti, Alley Stoughton, and Mayank Varia. Easyuc: Using easycrypt to mechanize proofs of universally composable security. In Proc. of CSF 2019, pages 167-183. IEEE, 2019. URL: https://doi.org/10.1109/CSF.2019.00019.
  15. Sara Capecchi, Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Tamara Rezk. Session types for access and information flow control. In Proc. of CONCUR 2010, volume 6269 of LNCS, pages 237-252. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_17.
  16. David Castro-Perez, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. Distributed programming using role-parametric session types in go: statically-typed endpoint apis for dynamically-instantiated communication structures. Proc. of POPL, 3:29:1-29:30, 2019. URL: https://doi.org/10.1145/3290342.
  17. Hubert Comon-Lundh, Masami Hagiya, Yusuke Kawamoto, and Hideki Sakurada. Computational soundness of indistinguishability properties without computable parsing. In Proc. of ISPEC 2012, volume 7232 of LNCS, pages 63-79. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-29101-2_5.
  18. Ugo Dal Lago and Paolo Di Giamberardino. On session types and polynomial time. Mathematical Structures in Computer Science, 26(8):1433-1458, 2016. URL: https://doi.org/10.1017/S0960129514000632.
  19. Ugo Dal Lago and Francesco Gavazzo. Resource transition systems and full abstraction for linear higher-order effectful programs. In Proc. of FSCD 2021, volume 195 of LIPIcs, pages 23:1-23:19, 2021. URL: https://doi.org/10.48550/arXiv.2106.12849.
  20. Ugo Dal Lago and Giulia Giusti. On session typing, probabilistic polynomial time, and cryptographic experiments (long version). Available at https://arxiv.org/abs/2207.03360, 2022.
  21. Ugo Dal Lago and Martin Hofmann. Bounded linear logic, revisited. Log. Methods Comput. Sci., 6(4), 2010. URL: https://doi.org/10.1007/978-3-642-02273-9_8.
  22. Ugo Dal Lago, Sara Zuppiroli, and Maurizio Gabbrielli. Probabilistic recursion theory and implicit computational complexity. Sci. Ann. Comput. Sci., 24(2):177-216, 2014. URL: https://doi.org/10.48550/arXiv.1406.3378.
  23. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. Inf. Comput., 256:253-286, 2017. URL: https://doi.org/10.1016/j.ic.2017.06.002.
  24. Ankush Das and Frank Pfenning. Session Types with Arithmetic Refinements. In Proc. of CONCUR 2020, volume 171, pages 13:1-13:18, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.13.
  25. Danny Dolev and Andrew Yao. On the security of public key protocols. IEEE, 29(2):198-208, 1983. URL: https://doi.org/10.1109/TIT.1983.1056650.
  26. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  27. Jean-Yves Girard, Andre Scedrov, and Philip J Scott. Bounded linear logic: a modular approach to polynomial-time computability. Theor. Comput. Sci., 97(1):1-66, 1992. URL: https://doi.org/10.1016/0304-3975(92)90386-T.
  28. Oded Goldreich. Foundations of Cryptography: Volume 1. Cambridge University Press, 2006. Google Scholar
  29. Martin Hofmann and Philip J. Scott. Realizability models for bll-like languages. Theor. Comput. Sci., 318(1-2):121-137, 2004. URL: https://doi.org/10.1016/j.tcs.2003.10.019.
  30. Kohei Honda. Types for dyadic interaction. In Proc. of CONCUR 1993, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  31. Hans Hüttel, Ivan Lanese, Vasco T Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, et al. Foundations of session types and behavioural contracts. ACM Computing Surveys (CSUR), 49(1):1-36, 2016. URL: https://doi.org/10.1145/2873052.
  32. Atsushi Igarashi, Peter Thiemann, Yuya Tsuda, Vasco T. Vasconcelos, and Philip Wadler. Gradual session types. J. Funct. Program., 29:e17, 2019. URL: https://doi.org/10.1017/S0956796819000169.
  33. Russell Impagliazzo and Bruce M. Kapron. Logics for reasoning about cryptographic constructions. J. Comput. Syst. Sci., 72(2):286-320, 2006. URL: https://doi.org/10.1016/j.jcss.2005.06.008.
  34. Omar Inverso, Hernán C. Melgratti, Luca Padovani, Catia Trubiani, and Emilio Tuosto. Probabilistic analysis of binary sessions. In Proc. of CONCUR 2020, volume 171 of LIPIcs, pages 14:1-14:21, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.14.
  35. Jonathan Katz and Yehuda Lindell. Introduction to modern cryptography. CRC press, 2020. Google Scholar
  36. Wen Kokke, J. Garrett Morris, and Philip Wadler. Towards races in linear logic. In Proc. of COORDINATION 2019, volume 11533 of LNCS, pages 37-53. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-22397-7_3.
  37. Ralf Küsters, Max Tuengerthal, and Daniel Rausch. The IITM model: A simple and expressive model for universal composability. J. Cryptol., 33(4):1461-1584, 2020. URL: https://doi.org/10.1007/s00145-020-09352-1.
  38. Kevin Liao, Matthew A. Hammer, and Andrew Miller. Ilc: a calculus for composable, computational cryptography. In Proc. of PLDI 2019, pages 640-654. ACM, 2019. URL: https://doi.org/10.1145/3314221.3314607.
  39. Patrick Lincoln, John C. Mitchell, Mark Mitchell, and Andre Scedrov. Probabilistic polynomial-time equivalence and security analysis. In Proc. of FM 1999, volume 1708 of LNCS, pages 776-793. Springer, 1999. URL: https://doi.org/10.1007/3-540-48119-2_43.
  40. John C. Mitchell, Mark Mitchell, and Andre Scedrov. A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In Proc. of FOCS 1998, pages 725-733. IEEE, 1998. URL: https://doi.org/10.1109/SFCS.1998.743523.
  41. John C. Mitchell, Ajith Ramanathan, Andre Scedrov, and Vanessa Teague. Probabilistic polynominal-time process calculus and security protocol analysis. In Proc. LICS 2001, pages 3-5. IEEE, 2001. URL: https://doi.org/10.1109/LICS.2001.932477.
  42. John C. Mitchell, Ajith Ramanathan, Andre Scedrov, and Vanessa Teague. A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theor. Comput. Sci., 353(1-3):118-164, 2006. URL: https://doi.org/10.1016/S1571-0661(04)80968-X.
  43. David Nowak and Yu Zhang. A calculus for game-based security proofs. In Proc. of RPROVSEC 2010, volume 6402 of LNCS, pages 35-52. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-16280-0_3.
  44. Jorge A Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Inf. Comput., 239:254-302, 2014. URL: https://doi.org/10.1016/j.ic.2014.08.001.
  45. Paula Severi, Luca Padovani, Emilio Tuosto, and Mariangiola Dezani-Ciancaglini. On sessions and infinite data. In Alberto Lluch-Lafuente and José Proença, editors, Proc. of COORDINATION 2016, volume 9686 of LNCS, pages 245-261. Springer, 2016. URL: https://doi.org/10.48550/arXiv.1610.06362.
  46. Jianxiong Shao, Yu Qin, and Dengguo Feng. Computational soundness results for stateful applied π calculus. In Proc. of POST 2016, volume 9635 of LNCS, pages 254-275. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49635-0_13.
  47. Bernardo Toninho, Luís Caires, and Frank Pfenning. Dependent session types via intuitionistic linear type theory. In Proc. of PPDP 2011, pages 161-172. ACM, 2011. URL: https://doi.org/10.1145/2003476.2003499.
  48. Philip Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384-418, 2014. URL: https://doi.org/10.1145/2398856.2364568.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact