Sessions and Separability in Security Protocols

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.