Vincent Cheval, Stéphanie Delaune, and Mark D. Ryan. Tests for establishing security properties. In Revised Selected Papers of the 9th Symposium on Trustworthy Global Computing (TGC'14), pp. 82–96, Lecture Notes in Computer Science 8902, Springer, Rome, Italy, December 2014.
Ensuring strong security properties in some cases requires participants to carry out tests during the execution of a protocol. A classical example is electronic voting: participants are required to verify the presence of their ballots on a bulletin board, and to verify the computation of the election outcome. The notion of certificate transparency is another example, in which participants in the protocol are required to perform tests to verify the integrity of a certificate log.
We present a framework for modelling systems with such `testable properties', using the applied pi calculus. We model the tests that are made by participants in order to obtain the security properties. Underlying our work is an attacker model called "malicious but cautious", which lies in between the Dolev-Yao model and the "honest but curious" model. The malicious-but-cautious model is appropriate for cloud computing providers that are potentially malicious but are assumed to be cautious about launching attacks that might cause user tests to fail.
@inproceedings{CDR-tgc14,
abstract = {Ensuring strong security properties in some cases
requires participants to carry out tests during the
execution of a protocol. A~classical example is
electronic voting: participants are required to
verify the presence of their ballots on a bulletin
board, and to verify the computation of the election
outcome. The notion of certificate transparency is
another example, in which participants in the
protocol are required to perform tests to verify the
integrity of a certificate log.\par We present a
framework for modelling systems with such `testable
properties', using the applied pi calculus. We model
the tests that are made by participants in order to
obtain the security properties. Underlying our work
is an attacker model called {"}malicious but
cautious{"}, which lies in between the Dolev-Yao
model and the {"}honest but curious{"} model. The
malicious-but-cautious model is appropriate for cloud
computing providers that are potentially malicious
but are assumed to be cautious about launching
attacks that might cause user tests to fail.},
address = {Rome, Italy},
author = {Cheval, Vincent and Delaune, St{\'e}phanie and
Ryan, Mark D.},
booktitle = {{R}evised {S}elected {P}apers of the 9th {S}ymposium
on {T}rustworthy {G}lobal {C}omputing ({TGC}'14)},
OPTDOI = {10.1007/978-3-662-45917-1_6},
editor = {Maffei, Matteo and Tuosto, Emilio},
month = dec,
pages = {82-96},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Tests for establishing security properties},
volume = {8902},
year = {2014},
acceptrate = {12/20},
acronym = {{TGC}'14},
nmonth = {12},
conf-month = sep,
lsv-category = {intc},
wwwpublic = {public and ccsb},
}