Provably Secure Certified Mail

Most cryptographic systems are defined reactively: there are multiple interactions between users and system, and both sides keep state between the interactions. So far there was no comprehensive and rigorously worked-out model supporting definitions and security proofs for such systems. Furthermore, there was no general methodology for the evaluation of practical protocols, which typically have imperfections that are tolerated for efficiency reasons, but would violate naive security definitions by ideal systems.

We propose such a model, following the simulation paradigm, and sketch a methodology to obtain practical security definitions that consider tolerable imperfections. As a non-trivial example we define certified mail as a reactive system (i.e., secure against active attacks), describe an optimistic certified mail protocol, and prove its security. This is the first rigorous proof at all for such a protocol, and probably, among the protocols yet proven in a setting with many interleaved executions, the one with the largest state space of the participants, which made it quite hard to get the distributed-systems aspects of the proof convincing. Our protocol is based on a known protocol, but in order to prove it secure we needed to modify it by using simulatability-friendly primitives like chameleon (or trap-door) commitments instead of committing encryption.

Specific aspects of our model are explicit users as stateful machines, which makes the model more intuitive and robust against composition, an exact timing model for this setting so that secure systems are also secure against certain timing channels, and independence from the trust model. As corroboration of the adequacy, we can show that our model is equivalent to several variants of it.