Execution Models for Choreographies and Cryptoprotocols

Marco Carbone, Joshua Guttman

    Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

    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
    Original languageEnglish
    JournalElectronic Proceedings in Theoretical Computer Science
    Issue number17
    Pages (from-to)1-11
    Number of pages11
    ISSN2075-2180
    Publication statusPublished - 2009

    Keywords

    • Choreographies
    • Transaction Models
    • Security Infrastructure
    • Cryptoprotocols
    • Execution Models

    Fingerprint

    Dive into the research topics of 'Execution Models for Choreographies and Cryptoprotocols'. Together they form a unique fingerprint.

    Cite this