ITU

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

Carbone, M & Guttman, J 2009, 'Execution Models for Choreographies and Cryptoprotocols', Electronic Proceedings in Theoretical Computer Science, no. 17, pp. 1-11.

APA

Carbone, M., & Guttman, J. (2009). Execution Models for Choreographies and Cryptoprotocols. Electronic Proceedings in Theoretical Computer Science, (17), 1-11.

Vancouver

Carbone M, Guttman J. Execution Models for Choreographies and Cryptoprotocols. Electronic Proceedings in Theoretical Computer Science. 2009;(17):1-11.

Author

Carbone, Marco ; Guttman, Joshua. / Execution Models for Choreographies and Cryptoprotocols. In: Electronic Proceedings in Theoretical Computer Science. 2009 ; No. 17. pp. 1-11.

Bibtex

@article{43baf2b0e62411dea523000ea68e967b,
title = "Execution Models for Choreographies and Cryptoprotocols",
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. Udgivelsesdato: 2009",
author = "Marco Carbone and Joshua Guttman",
year = "2009",
language = "English",
pages = "1--11",
journal = "Electronic Proceedings in Theoretical Computer Science",
issn = "2075-2180",
publisher = "Open Publishing Association",
number = "17",

}

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