Abstract
Process calculi are expressive specification languages for concurrency. They have been very successful in two research strands: (a) the analysis of security protocols and (b) the enforcement of correct message-passing programs. Despite their shared foundations, languages and reasoning techniques for (a) and (b) have been separately developed. Here we connect two representative calculi from (a) and (b): we encode a (high-level) \(\pi \)-calculus for multiparty sessions into a (low-level) applied \(\pi \)-calculus for security protocols. We establish the correctness of our encoding, and we show how it enables the integrated analysis of security properties and communication correctness by re-using existing tools.
Work partially funded by FAP-DF 0193.001381/2017.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of POPL 2001, pp. 104–115 (2001)
Bartoletti, M., Castellani, I., Deniélou, P., Dezani-Ciancaglini, M., Ghilezan, S., Pantovic, J., Pérez, J.A., Thiemann, P., Toninho, B., Vieira, H.T.: Combining behavioural types with security analysis. J. Log. Algebr. Meth. Program. 84(6), 763–780 (2015)
Blanchet, B.: Modeling and verifying security protocols with the applied Pi calculus and ProVerif. Found. Trends Priv. Secur. 1(1–2), 1–135 (2016)
Capecchi, S., Castellani, I., Dezani-Ciancaglini, M.: Typing access control and secure information flow in sessions. Inf. Comput. 238, 68–105 (2014)
Coppo, M., Dezani-Ciancaglini, M., Padovani, L., Yoshida, N.: A gentle introduction to multiparty asynchronous session types. In: Bernardo, M., Johnsen, E.B. (eds.) SFM 2015. LNCS, vol. 9104, pp. 146–178. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-18941-3_4
Corin, R., Deniélou, P., Fournet, C., Bhargavan, K., Leifer, J.J.: Secure implementations for typed session abstractions. In: Proceedings of CSF 2007, pp. 170–186. IEEE (2007)
Cortier, V., Kremer, S.: Formal models and techniques for analyzing security protocols: a tutorial. Found. Trends Program. Lang. 1(3), 151–267 (2014)
Garay, J.A., Jakobsson, M., MacKenzie, P.: Abuse-free optimistic contract signing. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 449–466. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48405-1_29
Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0053567
Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL, pp. 273–284 (2008)
Hüttel, H., Lanese, I., Vasconcelos, V.T., Caires, L., Carbone, M., Deniélou, P., Mostrous, D., Padovani, L., Ravara, A., Tuosto, E., Vieira, H.T., Zavattaro, G.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3 (2016)
Kremer, S., Künnemann, R.: Automated analysis of security protocols with global state. In: Proceedings of SP 2014, pp. 163–178. IEEE (2014)
Lowe, G.: Breaking and fixing the needham-schroeder public-key protocol using FDR. Softw. Concepts Tools 17(3), 93–102 (1996)
Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_48
Nantes, D., Pérez, J.A.: Relating process languages for security and communication correctness (full version). Technical report (2018). http://www.jperez.nl
Pfenning, F., Caires, L., Toninho, B.: Proof-carrying code in a session-typed process calculus. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 21–36. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25379-9_4
Acknowledgements
We are grateful to the anonymous reviewers for their useful remarks and suggestions. Pérez is also affiliated to the NOVA Laboratory for Computer Science and Informatics (supported by FCT grant NOVA LINCS PEst/UID/CEC/04516/2013), Universidade Nova de Lisboa, Portugal.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 IFIP International Federation for Information Processing
About this paper
Cite this paper
Nantes, D., Pérez, J.A. (2018). Relating Process Languages for Security and Communication Correctness (Extended Abstract). In: Baier, C., Caires, L. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2018. Lecture Notes in Computer Science(), vol 10854. Springer, Cham. https://doi.org/10.1007/978-3-319-92612-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-92612-4_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-92611-7
Online ISBN: 978-3-319-92612-4
eBook Packages: Computer ScienceComputer Science (R0)