Execution Models for Choreographies and Cryptoprotocols
Research output: Journal Article or Conference Article in Journal › Journal article › Research › peer-review
Standard
Execution Models for Choreographies and Cryptoprotocols. / Carbone, Marco; Guttman, Joshua.
In: Electronic Proceedings in Theoretical Computer Science, No. 17, 2009, p. 1-11.Research output: Journal Article or Conference Article in Journal › Journal article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - Execution Models for Choreographies and Cryptoprotocols
AU - Carbone, Marco
AU - Guttman, Joshua
PY - 2009
Y1 - 2009
N2 - 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. Udgivelsesdato: 2009
AB - 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. Udgivelsesdato: 2009
M3 - Journal article
SP - 1
EP - 11
JO - Electronic Proceedings in Theoretical Computer Science
JF - Electronic Proceedings in Theoretical Computer Science
SN - 2075-2180
IS - 17
ER -
ID: 1037906