# Relating Process Languages for Security and Communication Correctness (Extended Abstract)

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.
Document type :
Conference papers
Domain :
Complete list of metadata

Cited literature [16 references]

https://hal.inria.fr/hal-01824820
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Wednesday, June 27, 2018 - 3:55:40 PM
Last modification on : Wednesday, June 27, 2018 - 4:08:06 PM
Long-term archiving on: : Thursday, September 27, 2018 - 2:43:02 AM

### File

469043_1_En_5_Chapter.pdf
Files produced by the author(s)

### Citation

Daniele Nantes, Jorge A. Pérez. Relating Process Languages for Security and Communication Correctness (Extended Abstract). 38th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2018, Madrid, Spain. pp.79-100, ⟨10.1007/978-3-319-92612-4_5⟩. ⟨hal-01824820⟩

Record views