Simulation based security in the applied pi calculus

Abstract

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 the ``trusted
  party paradigm'' used in computational cryptography models. 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 show a joint state result for this
  functionality which allows composition (even though the same key
  material is reused) using a tagging mechanism.