Reliable Evidence: Auditability by Typing

Abstract. 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. 1 A language-based approach to auditing Consider a simple protocol where a client sends an authenticated mail to a server . To prove her identity, signs the message using her secret signing key and appends the signature to the message: Intuitively, this protocol guarantees the authenticity of the message sent by . The server can verify the signature using 's public key and, if the test succeeds, can be sure of the authenticity of the me...

• Type: Conference
• Year: 2009
• Where: ESORICS
• Authors: Nataliya Guts, Cédric Fournet, Francesco Zappa Nardelli
• Keywords: ESORICS 2009, Public Key, Secret Signing Key, Security Privacy, Sufficient Evidence