Track: Security, Privacy, Reliability and Ethics
Paper Title:
Compiling Cryptographic Protocols for Deployment on the Web
Authors:
Abstract:
Cryptographic protocols are useful for trust engineering in Web
transactions. The Cryptographic Protocol Programming Language
(CPPL) provides a model wherein trust management annotations are
attached to protocol actions, and are used to constrain the behavior
of a protocol participant to be compatible with its own trust
policy.
The first implementation of CPPL generated stand-alone, single-session servers, making it unsuitable for deploying protocols on the Web. We describe a new compiler that uses a constraint-based analysis to produce multi-session server programs. The resulting programs run without persistent TCP connections for deployment on traditional Web servers. Most importantly, the compiler preserves existing proofs about the protocols. We present an enhanced version of the CPPL language, discuss the generation and use of constraints, show their use in the compiler, formalize the preservation of properties, present subtleties, and outline implementation details.
