Authentication primitives and their compilation - Abadi, Martın; Fournet, Cédric; Gonthier, Georges (To appear in the Proceedings of the 27th ACM Symposium on Principles of Programming Languages (January 2000), 2000)
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 identity based security in the source language and enables simplifications in the translation. We reason about correctness relying on the concepts of observational equivalence and full abstraction.