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.


Published in:
Theoretical Computer Science, 389, 3, 484-511
Year:
2007
Keywords:
Other identifiers:
Laboratories:




 Record created 2007-01-09, last modified 2018-06-03

n/a:
Download fulltext
PDF

Rate this document:

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