Véronique Cortier and Stéphanie Delaune. Safely Composing Security Protocols. Formal Methods in System Design, 34(1):1–36, Springer, February 2009.
Security protocols are small programs that are executed in hostile environments. Many results and tools have been developed to formally analyze the security of a protocol in the presence of an active attacker that may block, intercept and send new messages. However even when a protocol has been proved secure, there is absolutely no guarantee if the protocol is executed in an environment where other protocols are executed, possibly sharing some common keys like public keys or long-term symmetric keys.
In this paper, we show that security of protocols can be easily composed. More precisely, we show that whenever a protocol is secure, it remains secure even in an environment where arbitrary protocols satisfying a reasonable (syntactic) condition are executed. This result holds for a large class of security properties that encompasses secrecy and various formulations of authentication.
@article{CD-fmsd08,
abstract = {Security protocols are small programs that are
executed in hostile environments. Many results and
tools have been developed to formally analyze the
security of a protocol in the presence of an active
attacker that may block, intercept and send new
messages. However even when a protocol has been
proved secure, there is absolutely no guarantee if
the protocol is executed in an environment where
other protocols are executed, possibly sharing some
common keys like public keys or long-term symmetric
keys.\par In this paper, we show that security of
protocols can be easily composed. More precisely, we
show that whenever a protocol is secure, it remains
secure even in an environment where arbitrary
protocols satisfying a reasonable (syntactic)
condition are executed. This result holds for a large
class of security properties that encompasses secrecy
and various formulations of authentication.},
author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
OPTDOI = {10.1007/s10703-008-0059-4},
journal = {Formal Methods in System Design},
month = feb,
number = {1},
pages = {1-36},
publisher = {Springer},
title = {Safely Composing Security Protocols},
volume = {34},
year = {2009},
nmonth = {2},
lsv-category = {jour},
wwwpublic = {public and ccsb},
}