Stéphanie Delaune, Steve Kremer, and Olivier Pereira. Simulation based security in the applied pi calculus. In Proceedings of the 29th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'09), pp. 169–180, Leibniz International Proceedings in Informatics 4, Leibniz-Zentrum für Informatik, Kanpur, India, December 2009.
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.
@inproceedings{DKP-fsttcs09,
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 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.},
address = {Kanpur, India},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Pereira, Olivier},
booktitle = {{P}roceedings of the 29th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience ({FSTTCS}'09)},
OPTDOI = {10.4230/LIPIcs.FSTTCS.2009.2316},
editor = {Kannan, Ravi and Narayan Kumar, K.},
month = dec,
pages = {169-180},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
title = {Simulation based security in the applied pi calculus},
volume = {4},
year = {2009},
acronym = {{FSTTCS}'09},
nmonth = {12},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}