Computational Indistinguishability Logic
Computational Indistinguishability Logic (CIL) is logic for reasoning about cryptographic primitives in computational models. It captures reasoning patterns that are common in provable security, such as simulations and reductions. CIL is sound for the standard model, but also supports reasoning in the random oracle and other idealized models. The authors illustrate the benefits of CIL by formally proving the security of the Probabilistic Signature Scheme (PSS).Cryptography plays a central role in the design of secure and reliable systems. Nevertheless, designing secure cryptographic schemes is notoriously hard.