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) π-calculus for multiparty sessions into a (low-level) applied π-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.

doi.org/10.1007/978-3-319-92612-4_5
Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence
International Conference on Formal Techniques for Distributed Objects, Components, and Systems

Nantes, D., & Pérez Parra, J. (2018). Relating process languages for security and communication correctness (extended abstract). In Proceedings of the International Conference on Formal Techniques for Distributed Objects, Components, and Systems (pp. 79–100). doi:10.1007/978-3-319-92612-4_5