fournet-et-al-2008-ESOP08-preprint-audit

A Formal Implementation of Value Commitment2;1 1 3;1Cedric´ Fournet , Nataliya Guts , and Francesco Zappa Nardelli1 MSR-INRIA Joint Centre2 Microsoft Research3 INRIAAbstract. In an optimistic approach to security, one can often simplify protocoldesign by relying on audit logs, which can be analyzed a posteriori. Such auditingis widely used in practice, but no formal studies guarantee that the log informa-tion suffices to reconstruct past runs of the protocol, in order to reliably detect(and provide evidence of) any cheating. We formalize audit logs for a sample op-timistic scheme, the value commitment. It is specified in a pi calculus extendedwith committable locations, and compiled using standard cryptography to imple-ment secure logs. We show that our distributed implementation either respectsthe abstract semantics of commitments or, using information stored in the logs,detects cheating by a hostile environment.1 A cautiously optimistic approach to securityMutual distrust in distributed computing makes enforcing system-wide security assur-ances particularly challenging. Common protocols perform an important number ofmandatory runtime checks and allow only legal computations to progress: in session-establishment protocols, for instance, a strong security invariant is usually enforced atevery step of the run of the protocol. These runtime checks have a cost, in terms ofcryptographic and networking operations; they may also conflict with other goals of ...