Sessions and Separability in Security Protocols

Marco Carbone, Joshua Guttman

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


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.
Original languageEnglish
Title of host publicationSecond International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013,
Number of pages20
PublisherSpringer Publishing Company
Publication date2013
ISBN (Print)978-3-642-36829-5
Publication statusPublished - 2013


Dive into the research topics of 'Sessions and Separability in Security Protocols'. Together they form a unique fingerprint.

Cite this