Compiling and securing cryptographic protocols

Protocol narrations are widely used in security as semi-formal notations to specify conversations between roles. We define a translation from a protocol narration to the sequences of operations to be performed by each role. Unlike previous works, we reduce this compilation process to well-known decision problems in formal protocol analysis. This allows one to define a natural notion of prudent translation and to reuse many known results from the literature in order to cover more crypto-primitives. In particular this work is the first one to show how to compile protocols parameterised by the properties of the available operations.

• Type: Journal
• Year: 2010
• Where: IPL
• Authors: Yannick Chevalier, Michaël Rusinowitch
• Keywords: Formal Protocol Analysis, IPL 2010, Protocol Narration, Well-known Decision Problems