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, wellmotivated 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.

• Type: Conference
• Year: 2005
• Where: TGC
• Authors: Sébastien Briais, Uwe Nestmann
• Keywords: Formal Protocol Descriptions, Protocol Narrations, Protocol’s Participants, TGC 2005