Title: 

A Multi-Role Translation of Protocol Narration into the Spi-Calculus
with Correspondence Assertions

Authors: 

Eijiro Sumii and Yuji Sato (Tohoku University)

Abstract:

We present an interpretation of protocol narrations by means of
translation into the spi-calculus.  Our translation allows
participants to play multiple roles in parallel, leading to a more
general interpretation that considers a wider range of attacks than
previous work.  We test the validity of our translation by introducing
correspondence assertions [Woo and Lam, S&P 1993] to both the protocol
narrations and the spi-calculus, and verifying a number of examples by
using SpiCA2 [Dahl, Kobayashi, Sun, and Hu"ttel, ATVA 2011], a sound
and automatic type-based verifier of correspondence assertions.