Paper 2009/267

Simulation based security in the applied pi calculus

Stéphanie Delaune, Steve Kremer, and Olivier Pereira


We present a symbolic framework for refinement and composition of security protocols. The framework uses the notion of ideal functionalities. These are abstract systems which are secure by construction and which can be combined into larger systems. They can be separately refined in order to obtain concrete protocols implementing them. Our work builds on ideas from computational models such as the universally composable security and reactive simulatability frameworks. The underlying language we use is the applied pi calculus which is a general language for specifying security protocols. In our framework we can express the different standard flavours of simulation-based security which happen to all coincide. We illustrate our framework on an authentication functionality which can be realized using the Needham-Schroeder-Lowe protocol. For this we need to define an ideal functionality for asymmetric encryption and its realization. We also show a joint state result for this functionality which allows composition (even though the same key material is reused) using a tagging mechanism.

Available format(s)
Publication info
Published elsewhere. Unknown where it was published
Contact author(s)
kremer @ lsv ens-cachan fr
2009-06-09: received
Short URL
Creative Commons Attribution


      author = {Stéphanie Delaune and Steve Kremer and Olivier Pereira},
      title = {Simulation based security in the applied pi calculus},
      howpublished = {Cryptology ePrint Archive, Paper 2009/267},
      year = {2009},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.