A Protocol Compiler for Secure Sessions in ML

R.J. Corin, P-M. Denielou

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    7 Citations (Scopus)
    1 Downloads (Pure)


    Distributed applications can be structured using sessions that specify flows of messages between roles. We design a small specific language to declare sessions. We then build a compiler, called s2ml, that transforms these declarations down to ML modules securely implementing the sessions. Every run of a well-typed program executing a session through its generated module is guaranteed to follow the session specification, despite any low-level attempt by coalitions of remote peers to deviate from their roles. We detail the inner workings of our compiler, along with our design choices, and illustrate the usage of s2ml with two examples: a simple remote procedure call session, and a complex session for a conference management system.
    Original languageUndefined
    Title of host publication3rd Symposium on Trustworthy Global Computing (TGC) Revised Selected Papers
    EditorsG. Barthe, C. Fournet
    Place of PublicationLondon
    Number of pages23
    ISBN (Print)978-3-540-78662-7
    Publication statusPublished - 5 Nov 2007
    Event3rd Symposium on Trustworthy Global Computing 2007 - Sophia-Antipolis, Valbonne, France
    Duration: 5 Nov 20076 Nov 2007
    Conference number: 3

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag


    Conference3rd Symposium on Trustworthy Global Computing 2007
    Abbreviated titleTGC 2007


    • EWI-11180
    • IR-61955
    • SCS-Cybersecurity
    • METIS-241969

    Cite this