Authentication Primitives and Their Compilation

Adopting a programming-language perspective, we study the problem of implementing authentication in a distributed system. We define a process calculus with constructs for authentication and show how this calculus can be translated to a lower-level language using marshaling, multiplexing, and cryptographic protocols. Authentication serves for identitybased security in the source language and enables simplifications in the translation. We reason about correctness relying on the concepts of observational equivalence and full ion. 1 Authenticity from a programming-language perspective Establishing the origins and the destinations of messages is a common problem in distributed systems. When security matters, the solutions to the problem rely on sophisticated mechanisms such as authentication protocols, digital signatures, and encryption [25]. From the perspective of programming languages [28], we may rephrase the problem and its solutions in the following general terms: • First, we hav...

• Type: Conference
• Year: 2000
• Where: POPL
• Authors: Martín Abadi, Cédric Fournet, Georges Gonthier
• Keywords: Authentication, Distributed Systems, POPL 2000, Programming Languages, Programming-language Perspective