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.


Published in:
Proceedings (Revised Selected Papers) of Trustworthy Global Computing, 163-181
Presented at:
Trustworthy Global Computing, Edinburgh, April 7-9 2005
Year:
2005
Keywords:
Laboratories:




 Record created 2006-04-28, last modified 2018-03-17

External link:
Download fulltext
URL
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)