Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations

We 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 id...

Full description

Bibliographic Details
Main Author: Almeida, José Bacelar (author)
Other Authors: Barbosa, Manuel (author), Barthe, Gilles Jacques Denis (author), Dupressoir, François (author)
Format: conferencePaper
Language:eng
Published: 2013
Subjects:
certified compilation
formal proof
PKCS#1
side-channels
Online Access:http://hdl.handle.net/1822/36148
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/36148

Internet

http://hdl.handle.net/1822/36148

Similar Items