Sciweavers

CORR
2009
Springer

Execution Models for Choreographies and Cryptoprotocols

13 years 1 months ago
Execution Models for Choreographies and Cryptoprotocols
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.
Marco Carbone, Joshua D. Guttman
Added 17 Feb 2011
Updated 17 Feb 2011
Type Journal
Year 2009
Where CORR
Authors Marco Carbone, Joshua D. Guttman
Comments (0)