1 Programming, Logic and Semantics, Software & Systems, The Department2 Theoretical Computer Science, The Department3 Process and System Models, Software & Systems, The Department4 Programming Logic and Semantics, Theoretical Computer Science, The Department5 Computer Science, IT University of Copenhagen6 Worcester Polytechnic Institute7 Worcester Polytechnic Institute
Despite much work on sessions and session types in non- adversarial contexts, session-like behavior given an active adversary has not received an adequate definition and proof methods. We provide a syntactic property that guarantees that a protocol has session-respecting executions. Any uncompromised subset of the participants are still guar- anteed that their interaction will respect sessions. A protocol transfor- mation turns any protocol into a session-respecting protocol. We do this via a general theory of separability. Our main theorem ap- plies to different separability requirements, and characterizes when we can separate protocol executions sufficiently to meet a particular require- ment. This theorem also gives direct proofs of some old and new protocol composition results. Thus, our theory of separability appears to cover protocol composition and session-like behavior within a uniform frame- work, and gives a general pattern for reasoning about independence.
Second International Conference, Post 2013, Held As Part of the European Joint Conferences on Theory and Practice of Software, Etaps 2013,, 2013, p. 267-286