Adopting a programming-language perspective, we study the problem of implementing authentication in a distributed system. We defien 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 identity-based security in the source language and enables simpli-fications in the translation. We reason about correctness relying on the concepts of observational equivalence and full abstraction.
展开▼
