ITU

Choreographies with Secure Boxes and Compromised Principals

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

Standard

Choreographies with Secure Boxes and Compromised Principals. / Carbone, Marco; Guttman, Joshua.

In: Electronic Proceedings in Theoretical Computer Science, No. 12, 2009, p. 1-15.

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

Harvard

APA

Vancouver

Author

Bibtex

@inproceedings{021937205f2111de8664000ea68e967b,
title = "Choreographies with Secure Boxes and Compromised Principals",
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 A′ is accessible from A, then A′ is minimal. Thus, the transition system provides a systematic way to construct the possible behaviors of the choreography, in the presence of compromised principals. ",
author = "Marco Carbone and Joshua Guttman",
note = "Udgivelsesdato: 29.11.2009; null ; Conference date: 31-08-2009 Through 31-08-2009",
year = "2009",
doi = "10.4204/EPTCS.12.1",
language = "English",
pages = "1--15",
journal = "Electronic Proceedings in Theoretical Computer Science",
issn = "2075-2180",
publisher = "Open Publishing Association",
number = "12",

}

RIS

TY - GEN

T1 - Choreographies with Secure Boxes and Compromised Principals

AU - Carbone, Marco

AU - Guttman, Joshua

N1 - Conference code: 2

PY - 2009

Y1 - 2009

N2 -  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 A′ is accessible from A, then A′ is minimal. Thus, the transition system provides a systematic way to construct the possible behaviors of the choreography, in the presence of compromised principals. 

AB -  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 A′ is accessible from A, then A′ is minimal. Thus, the transition system provides a systematic way to construct the possible behaviors of the choreography, in the presence of compromised principals. 

U2 - 10.4204/EPTCS.12.1

DO - 10.4204/EPTCS.12.1

M3 - Conference article

SP - 1

EP - 15

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

IS - 12

Y2 - 31 August 2009 through 31 August 2009

ER -

ID: 992215