Choreographies with Secure Boxes and Compromised Principals

Marco Carbone, Joshua Guttman

    Publikation: Artikel i tidsskrift og konference artikel i tidsskriftKonferenceartikelForskningpeer review

    Abstract

     

    We equip choreography-level session descriptions with a simple abstraction of a security infrastruc- ture. Message components may be enclosed within (possibly nested) ”boxes” annotated with the intended source and destination of those components. The boxes are to be implemented with cryp- tography.

    Strand spaces provide a semantics for these choreographies, in which some roles may be played by compromised principals. A skeleton is a partially ordered structure containing local behaviors (strands) executed by regular (non-compromised) principals. A skeleton is realized if it contains enough regular strands so that it could actually occur, in combination with any possible activity of compromised principals. It is delivery guaranteed (DG) realized if, in addition, every message transmitted to a regular participant is also delivered.

    We define a novel transition system on skeletons, in which the steps add regular strands. These steps solve tests, i.e. parts of the skeleton that could not occur without additional regular behavior.

    We prove three main results about the transition system. First, each minimal DG realized skeleton is reachable, using the transition system, from any skeleton it embeds. Second, if no step is possible from a skeleton A, then A is DG realized. Finally, if a DG realized Ais accessible from A, then Ais minimal. Thus, the transition system provides a systematic way to construct the possible behaviors of the choreography, in the presence of compromised principals.

     

    OriginalsprogEngelsk
    TidsskriftElectronic Proceedings in Theoretical Computer Science
    Udgave nummer12
    Sider (fra-til)1-15
    Antal sider15
    ISSN2075-2180
    DOI
    StatusUdgivet - 2009
    BegivenhedICE 2009 - 2nd Interaction and Concurrency Experience - Bologna, Italien
    Varighed: 31 aug. 200931 aug. 2009
    Konferencens nummer: 2

    Konference

    KonferenceICE 2009 - 2nd Interaction and Concurrency Experience
    Nummer2
    Land/OmrådeItalien
    ByBologna
    Periode31/08/200931/08/2009

    Emneord

    • Choreography-level session descriptions
    • Security infrastructure
    • Strand spaces
    • Delivery guaranteed realized
    • Transition system on skeletons

    Citationsformater