Reasoning about concurrency for security tunnels

Alwyn E. Goodloe, Carl A. Gunter

Research output: Chapter in Book/Report/Conference proceedingConference contribution


There has been excellent progress on languages for rigorously describing key exchange protocols and techniques for proving that the network security tunnels they establish preserve confidentiality and integrity. New problems arise in describing and analyzing establishment protocols and tunnels when they are used as building blocks to achieve high-level security goals for network administrative domains. We introduce a language called the tunnel calculus and associated analysis techniques that can address functional problems arising in the concurrent establishment of tunnels. In particular, we use the tunnel calculus to explain and resolve cases where interleavings of establishment messages can lead to deadlock. Deadlock can be avoided by making unwelcome security compromises, but we prove that it can be eliminated systematically without such compromises using a concept of session to relate tunnels. Our main results are noninterference and progress theorems familiar to the concurrency community, but not previously applied to tunnel establishment protocols.

Original languageEnglish (US)
Title of host publicationProceedings - 20th IEEE Computer Security Foundations Symposium, CSFS20
Number of pages15
StatePublished - 2007
Event20th IEEE Computer Security Foundations Symposium, CSFS20 - Venice, Italy
Duration: Jul 6 2007Jul 8 2007

Publication series

NameProceedings - IEEE Computer Security Foundations Symposium
ISSN (Print)1940-1434


Other20th IEEE Computer Security Foundations Symposium, CSFS20

ASJC Scopus subject areas

  • Engineering(all)


Dive into the research topics of 'Reasoning about concurrency for security tunnels'. Together they form a unique fingerprint.

Cite this