Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC

DOI10.1007/978-3-662-52993-5_9MaRDI QIDQ4639476zbMATH OpenOpenAlexFDO

Authors Manuel Barbosa, Gilles Barthe, François Dupressoir, José Bacelar Almeida

Publication date 9 May 2018

Published in Fast Software Encryption (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/1822/51554

zbMATH Keywords

block cipherleakage modelprovable securityrandom coinsecurity notion

Mathematics Subject Classification ID

Cryptography (94A60)

Recommendations

• Lucky microseconds: a timing attack on Amazon's s2n implementation of TLS
• Verifying constant-time implementations by abstract interpretation
• Formal verification of side-channel countermeasures via elementary circuit transformations
• System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
• System-level non-interference of constant-time cryptography. I: Model

Cites work

• Advances in Cryptology - CRYPTO 2003
• Computer-Aided Security Proofs for the Working Cryptographer
• EasyCrypt: a tutorial
• Faster and Timing-Attack Resistant AES-GCM
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• scientific article; zbMATH DE number 1583804 (Why is no real title available?)
• scientific article; zbMATH DE number 2086729 (Why is no real title available?)
• scientific article; zbMATH DE number 1842499 (Why is no real title available?)
• Lucky microseconds: a timing attack on Amazon's s2n implementation of TLS
• On symmetric encryption with distinguishable decryption failures
• Rogue Decryption Failures: Reconciling AE Robustness Notions
• Security of symmetric encryption against mass surveillance
• System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory
• Tag size does matter: attacks and proofs for the TLS record protocol
• The security impact of a new cryptographic library

Cited in

(8)

• Certified compilation for cryptography: extended x86 instructions and constant-time verification
• Verifying constant-time implementations by abstract interpretation
• System-level non-interference of constant-time cryptography. I: Model
• Lucky microseconds: a timing attack on Amazon's s2n implementation of TLS
• Towards Side-Channel Resistant Implementations of QC-MDPC McEliece Encryption on Constrained Devices
• Output-sensitive information flow analysis
• New versions of Miller-loop secured against side-channel attacks
• Formally verifying Kyber. Episode V: machine-checked IND-CCA security and correctness of ML-KEM in Easycrypt

Describes a project that uses

Uses Software

• s2n
• OpenSSL

This page was built for publication: Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4639476)