Formal Properties of Audit Logs

Many protocols rely on secure audit logs to store traces of protocol runs. These logs can be used a posteriori to verify the compliance of each principal to its role: principals who attempt non-compliant actions will be blamed using the logged evidence. Secure logging is widely used in standard practice. Much research effort has been devoted to techniques for implementing logs so as to guarantee properties such as correctness, forward integrity, and forward secrecy.

Still, which data should be logged? and why? Between general recommendations such as "an audit trail should include sufficient information to establish what events occurred and who (or what) caused them" and efficient implementation techniques, we are not aware of any formal studies that characterize and verify the security properties achieved by protocols relying of logs. We attempt to formally answer this question.

Papers and Talks

New! Reliable Evidence: Auditability by Typing. Submitted to ESORICS'09.

Source code and instructions for use of the examples are available here.

In current practice the choice of what data to log is left to the programmer's intuition. 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 to verify a posteriori some property of a protocol run. We apply our approach to several examples, including a full-scale auction-like protocol programmed in ML.

A Formal Implementation of Value Commitment. In ESOP'08, vol. 4960 of LNCS, pp.383-397, Springer, 2008.

In this paper, we formalize audit logs for a sample optimistic scheme, the value commitment. It is specified in a pi calculus extended with committable locations, and compiled using standard cryptography to implement secure logs. We show that our distributed implementation either respects the abstract semantics of commitments or, using the information stored in the logs, detects cheating by a hostile environment.

See also the ESOP'08 slides, an extended version of the paper including full language definitions.

People

Cédric Fournet, Nataliya Guts and Francesco Zappa Nardelli.

Related

NIST: Generally accepted principles and practices for securing information technology systems

ISO/IEC: Common criteria for information technology security evaluation

Audit-based compliance control (University of Twente)

Evidence-based Audit (University of Pennsylvania)