Relating Process Languages for Security and Communication Correctness

Process calculi are expressive specification languages for concurrency. They have been very successful in two research strands:

1. the analysis of security protocols and
2. the enforcement of correct message-passing programs.

Despite their shared foundations, languages and reasoning techniques for (1) and (2) have been separately developed.

Here we connect two representative calculi from (1) and (2): 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