Choreographies With Secure Boxes and Compromised Principals
Source: Creative Commons
The authors equip choreography-level session descriptions with a simple abstraction of a security infrastructure. 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 cryptography. Strand spaces provide 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.