Execution Models for Choreographies and Cryptoprotocols

TL;DR

This paper develops execution models for choreographies and cryptoprotocols, ensuring secure, faithful message delivery and handling compromised participants, to facilitate safe business process implementations.

Contribution

It introduces a strand-style semantics for choreographies and adapts the at-most-once delivery model for cryptoprotocols with nonce caches, enhancing security analysis.

Findings

A faithful one-time delivery model for choreography messages.

An adapted Dolev-Yao model for at-most-once cryptoprotocol execution.

Framework for analyzing security in multiparty protocols with compromised participants.

Abstract

A choreography describes a transaction in which several principals interact. Since choreographies frequently describe business processes affecting substantial assets, we need a security infrastructure in order to implement them safely. As part of a line of work devoted to generating cryptoprotocols from choreographies, we focus here on the execution models suited to the two levels. We give a strand-style semantics for choreographies, and propose a special execution model in which choreography-level messages are faithfully delivered exactly once. We adapt this model to handle multiparty protocols in which some participants may be compromised. At level of cryptoprotocols, we use the standard Dolev-Yao execution model, with one alteration. Since many implementations use a "nonce cache" to discard multiply delivered messages, we provide a semantics for at-most-once delivery.