|
|
Abstract:
A "proof" in cryptography is often a reduction of a security definition to some computationally hard problem. The security definition consists of a game (which can be thought as a probabilistic imperative program) between an unknown polynomial-time adversary and a challenger. The reduction is usually done by constructing a probabilistic program that uses the output of the adversary to solve the computationally hard problem, and it is called a "simulation". We present an informal method to organize a simulation-based proof as a sequence of game transformations. We apply this technique to prove the security of the Identity Based Encryption (IBE) scheme of Boneh and Boyen and to show its similarities with the IBE scheme of Waters. A relational probabilistic Hoare-like logic to perform code-based transformations in a rigorous way is introduced.
|