%0 Conference Proceedings
%T Relating Process Languages for Security and Communication Correctness (Extended Abstract)
%+ Universidade Católica de Brasília=Catholic University of Brasília (UCB)
%+ Centrum Wiskunde & Informatica (CWI)
%+ University of Groningen [Groningen]
%A Nantes, Daniele
%A Pérez, Jorge, A.
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 38th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Madrid, Spain
%Y Christel Baier
%Y Luís Caires
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-10854
%P 79-100
%8 2018-06-18
%D 2018
%R 10.1007/978-3-319-92612-4_5
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01824820/document
%2 https://inria.hal.science/hal-01824820/file/469043_1_En_5_Chapter.pdf
%L hal-01824820
%U https://inria.hal.science/hal-01824820
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-DISCOTEC
%~ IFIP-LNCS-10854