ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Thirteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1998)

Paper: Secure Implementation of Channel Abstractions (at LICS 1998)

Winner of the Test-of-Time Award in 2018
Authors: Martín Abadi Cédric Fournet Georges Gonthier


Communication in distributed systems often relies on useful abstractions such as channels, remote procedure calls, and remote method invocations. The implementations of these abstractions sometimes provide security properties, in particular through encryption. In this paper we study those security properties, focusing on channel abstractions. We introduce a simple high-level language that includes constructs for creating and using secure channels. The language is a variant of the join-calculus and belongs to the same family as the pi-calculus. We show how to translate the high-level language into a lower-level language that includes cryptographic primitives. In this translation, we map communication on secure channels to encrypted communication on public channels. We obtain a correctness theorem for our translation; this theorem implies that one can reason about programs in the high-level language without mentioning the subtle cryptographic protocols used in their lower-level implementation


    author = 	 {Martín Abadi and Cédric Fournet and Georges Gonthier},
    title = 	 {Secure Implementation of Channel Abstractions},
    booktitle =  {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)},
    year =	 {1998},
    month =	 {June}, 
    pages =      {105--116},
    location =   {Indianapolis, IN, USA}, 
    publisher =	 {IEEE Computer Society Press}

Last modified: 2022-10-3113:49
Sam Staton