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 guaranteed that their interaction will respect sessions. A protocol transformation turns any protocol into a session-respecting protocol. We do this via a general theory of separability. Our main theorem applies to different separability requirements, and characterizes when we can separate protocol executions sufficiently to meet a particular requirement. 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 framework, and gives a general pattern for reasoning about independence. © 2013 Springer-Verlag.
CITATION STYLE
Carbone, M., & Guttman, J. D. (2013). Sessions and separability in security protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7796 LNCS, pp. 267–286). https://doi.org/10.1007/978-3-642-36830-1_14
Mendeley helps you to discover research relevant for your work.