Certified Computer-Aided Cryptography: Efficient Provably Secure Machine Code From High-Level Implementations

The authors present a computer-aided framework for proving concrete security bounds for cryptographic machine code implementations. The front-end of the framework is an interactive verification tool that extends the EasyCrypt framework to reason about relational properties of C-like programs extended with idealized probabilistic operations in the style of code-based security proofs. The framework also incorporates an extension of the CompCert certified compiler to support trusted libraries providing complex arithmetic calculations or instantiating idealized components such as sampling operations.

Provided by: IMDEA Topic: Security Date Added: May 2013 Format: PDF

Find By Topic