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

Daniele Nantes, Jorge A. Pérez

Research output: Contribution to conferencePaperAcademic

184 Downloads (Pure)

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) π -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.
Original languageEnglish
Pages79-100
Number of pages22
DOIs
Publication statusPublished - 2018
Event38th IFIP WG 6.1 International Conference, FORTE 2018 - Madrid, Spain
Duration: 18-Jun-201821-Jun-2018

Conference

Conference38th IFIP WG 6.1 International Conference, FORTE 2018
Country/TerritorySpain
CityMadrid
Period18/06/201821/06/2018

Cite this