A Protocol Compiler for Secure Sessions in ML

  • Ricardo Corin
  • Pierre-Malo Deniélou
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4912)


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.


Cryptographic Protocol User Code Session Type Local Role Visible Sequence 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bhargavan, K., Corin, R., Fournet, C., Gordon, A.D.: Secure sessions for web services. In: ACM Workshop on Secure Web Services (SWS), pp. 11–22 (October 2004)Google Scholar
  2. 2.
    Bhargavan, K., Fournet, C., Gordon, A.D., Tse, S.: Verified interoperable implementations of security protocols. In: 19th IEEE Computer Security Foundations Workshop (CSFW), July 2006, pp. 139–152 (2006)Google Scholar
  3. 3.
    J. Billings, P. Sewell, M. Shinwell, and R. Strniša. Type-Safe Distributed Programming for OCaml. In: ACM SIGPLAN Workshop on ML, September 2006 (2006)Google Scholar
  4. 4.
    Bonelli, E., Compagnoni, A., Gunter, E.: Correspondence assertions for process synchronization in concurrent communications. In: Brogi, A. (ed.) 1st International Workshop on Foundations of Coordination Languages and Software Architectures (FOCLASA). ENTCS, vol. 97, pp. 175–195. Elsevier, Amsterdam (2004)Google Scholar
  5. 5.
    Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, Springer, Heidelberg (2007)CrossRefGoogle Scholar
  6. 6.
    Carpineti, S., Laneve, C.: A basic contract language for web services. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 197–213. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: model checking message-passing programs. In: 29th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL), January 2002, pp. 45–57 (2002)Google Scholar
  8. 8.
    Corin, R., Denielou, P.M., Fournet, C., Bhargavan, K., Leifer, J.: Secure implementations for typed session abstractions. In: 20th IEEE Computer Security Foundations Symposium (CSF 2007), Venice, Italy, July 2007, IEEE Computer Society Press, Los Alamitos (to appear, 2007)Google Scholar
  9. 9.
    Corin, R., Dénielou, P.-M., Fournet, C., Bhargavan, K., Leifer, J.: Secure sessions project (2007),
  10. 10.
    Deniélou, P.-M., Leifer, J.J.: Abstraction preservation and subtyping in distributed languages. In: 11th International Conference on Functional Programming (ICFP) (2006)Google Scholar
  11. 11.
    Dezani-Ciancaglini, M., Mostrous, D., Yoshida, N., Drossopoulou, S.: Session types for object-oriented languages. In: 20th European Conference for Object-Oriented Languages, July 2006 (2006)Google Scholar
  12. 12.
    Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
  14. 14.
    Fahndrich, M., Aiken, M., Hawblitzel, C., Hodson, G.H.O., Larus, J.R., Levi, S.: Language support for fast and reliable message-based communication in Singularity OS. In: EUROSYS (2006)Google Scholar
  15. 15.
    Simon, J.: Gay and Malcolm Hole. Types and subtypes for client-server interactions. In: Programming Languages and Systems, 8th European Symposium on Programming (ESOP), pp. 74–90 (1999)Google Scholar
  16. 16.
    Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. Journal of Computer Security 11(4), 451–521 (2003)Google Scholar
  17. 17.
    Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type disciplines for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998 and ETAPS 1998. LNCS, vol. 1381, pp. 22–138. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  18. 18.
    Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008 (to appear, 2008)Google Scholar
  19. 19.
    Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. In: 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL), pp. 128–141 (2001)Google Scholar
  20. 20.
    Milner, R., Tofte, M., Harper, R.: The Definition of Standard ML. MIT Press, Cambridge (1990)Google Scholar
  21. 21.
    Objective Caml,
  22. 22.
    Sewell, P., Leifer, J.J., Wansbrough, K., Nardelli, F.Z., Allen-Williams, M., Habouzit, P., Vafeiadis, V.: Acute: High-level programming language design for distributed computation. In: 10th International Conference on Functional Programming (ICFP), September 2005 (2005)Google Scholar
  23. 23.
  24. 24.
    Vallecillo, A., Vasconcelos, V.T., Ravara, A.: Typing the behavior of objects and components using session types. In: 1st International Workshop on Foundations of Coordination Languages and Software Architectures (FOCLASA). ENTCS, vol. 68, Elsevier, Amsterdam (2003)Google Scholar
  25. 25.
    Vasco, T.: Vasconcelos, Simon Gay, and António Ravara. Typechecking a multithreaded functional language with session types, TCS 368(1–2), 64–87 (2006)zbMATHGoogle Scholar
  26. 26.
    Yoshida, N., Vasconcelos, V.T.: Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. In: 1st International Workshop on Security and Rewriting Techniques, ENTCS (2006)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Ricardo Corin
    • 1
    • 2
  • Pierre-Malo Deniélou
    • 1
  1. 1.MSR-INRIA Joint Centre 
  2. 2.University of Twente 

Personalised recommendations