Sessions and Separability in Security Protocols

Marco Carbone, Joshua Guttman

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer 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.
TitelSecond International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013,
Antal sider20
ForlagSpringer Publishing Company
ISBN (Trykt)978-3-642-36829-5
StatusUdgivet - 2013


Dyk ned i forskningsemnerne om 'Sessions and Separability in Security Protocols'. Sammen danner de et unikt fingeraftryk.