Publication
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.