A Formal Implementation of Value Commitment

In an optimistic approach to security, one can often simplify protocol design by relying on audit logs, which can be analyzed a posteriori. Such auditing is widely used in practice, but no formal studies guarantee that the log information 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 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 ract semantics of commitments or, using information stored in the logs, detects cheating by a hostile environment. 1 A cautiously optimistic approach to security Mutual distrust in distributed computing makes enforcing system-wide security assurances particularly challenging. Common protocols perform an important number of mandatory runtime checks and allow only le...

• Type: Conference
• Year: 2008
• Where: ESOP
• Authors: Cédric Fournet, Nataliya Guts, Francesco Zappa Nardelli
• Keywords: Audit Logs, ESOP 2008, Optimistic Approach, Programming Languages, Runtime Checks