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