A Secure Compiler for Session Abstractions

In Journal of Computer Security, 2008-11-19, p. 573-636, joint work with Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, and James Leifer.

Abstract

This full paper merges the results from the following two papers, provides the proofs, and includes additional details and examples.

Journal version

A pre-print is available [ pdf ].

References

• A protocol compiler for secure sessions in ML (TGC'07) [A protocol compiler for secure sessions in ML].
• Secure Implementations for Typed Session Abstractions (CSF'07) [A Secure Compiler for Session Abstractions].