Compiling and securing cryptographic protocols

TL;DR

This paper introduces a method to compile cryptographic protocols from semi-formal narrations into operational sequences, leveraging formal analysis techniques to enhance security and flexibility.

Contribution

It presents a novel translation approach from protocol narrations to operational sequences, reducing the process to known decision problems and enabling compilation based on operation properties.

Findings

First to compile parameterized protocols based on operation properties

Reduces compilation to well-known decision problems

Enables reuse of formal analysis results for protocol security

Abstract

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.