TY - GEN
T1 - Reliable evidence
T2 - 14th European Symposium on Research in Computer Security, ESORICS 2009
AU - Guts, Nataliya
AU - Fournet, Cédric
AU - Zappa Nardelli, Francesco
PY - 2009/11/2
Y1 - 2009/11/2
N2 - Many protocols rely on audit trails to allow an impartial judge to verify a posteriori some property of a protocol run. However, in current practice the choice of what data to log is left to the programmer's intuition, and there is no guarantee that it constitutes enough evidence. We give a precise definition of auditability and we show how typechecking can be used to statically verify that a protocol always logs enough evidence. We apply our approach to several examples, including a full-scale auction-like protocol programmed in ML.
AB - Many protocols rely on audit trails to allow an impartial judge to verify a posteriori some property of a protocol run. However, in current practice the choice of what data to log is left to the programmer's intuition, and there is no guarantee that it constitutes enough evidence. We give a precise definition of auditability and we show how typechecking can be used to statically verify that a protocol always logs enough evidence. We apply our approach to several examples, including a full-scale auction-like protocol programmed in ML.
UR - https://www.scopus.com/pages/publications/70350353223
U2 - 10.1007/978-3-642-04444-1_11
DO - 10.1007/978-3-642-04444-1_11
M3 - Conference contribution
AN - SCOPUS:70350353223
SN - 3642044433
SN - 9783642044434
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 168
EP - 183
BT - Computer Security - ESORICS 2009 - 14th European Symposium on Research in Computer Security, Proceedings
Y2 - 21 September 2009 through 23 September 2009
ER -