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. © 2009 Springer Berlin Heidelberg.
CITATION STYLE
Guts, N., Fournet, C., & Zappa Nardelli, F. (2009). Reliable evidence: Auditability by typing. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5789 LNCS, pp. 168–183). https://doi.org/10.1007/978-3-642-04444-1_11
Mendeley helps you to discover research relevant for your work.