A Formal Semantics For Protocol Narrations

Protocol narrations are a widely-used 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. An optimised translation has been implemented in OCaml, and we report on case studies that we have carried out using the tool.


Year:
2006
Keywords:
Note:
preprint submitted to Elsevier Science
Laboratories:




 Record created 2006-12-20, last modified 2018-03-17

n/a:
Download fulltext
PDF

Rate this document:

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