Infoscience

Conference paper

# A Formal Semantics For Protocol Narrations

Protocol narrations are an informal means to describe, in an idealistic manner, the functioning of cryptographic protocols as a single intended sequence of cryptographic message exchanges among the protocol's participants. Protocol narrations have also been informally turned into'' a number of formal protocol descriptions, e.g., using the spi calculus. In this paper, we propose a direct formal operational semantics for protocol narrations that fixes a particular and, as we argue, well-motivated interpretation on how the involved protocol participants are supposed to execute. Based on this semantics, we explain and formally justify a natural and precise translation of narrations into spi-calculus.

#### Reference

• LAMP-CONF-2006-001

Record created on 2006-04-28, modified on 2016-08-08