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). Proceedings of the International Conference on Formal Techniques for Distributed Objects, Components, and Systems, 10854.https://doi.org/10.1007/978-3-319-92612-4_5