Automated proofs of block cipher modes of operation

DOI10.1007/S10817-015-9341-5MaRDI QIDQ287326zbMATH OpenOpenAlexWikidataFDO

Authors Martin Gagné, Pascal Lafourcade, Reihaneh Safavi-Naini, Yassine Lakhnech

Publication date 26 May 2016

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-015-9341-5

zbMATH Keywords

block cipherautomated verificationHoare logicprovable cryptographysymmetric encryption

Mathematics Subject Classification ID

Cryptography (94A60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Recommendations

• Automated verification of block cipher modes of operation, an improved method
• Automated security proof for symmetric encryption modes
• Automated proofs for asymmetric encryption
• Automated proofs for asymmetric encryption
• scientific article; zbMATH DE number 2086169
• On modes of operations of a block cipher for authentication and authenticated encryption
• Automated verification of equivalence properties of cryptographic protocols
• Automated verification of equivalence properties of cryptographic protocols

Cites work

• scientific article; zbMATH DE number 1722692 (Why is no real title available?)
• scientific article; zbMATH DE number 2089141 (Why is no real title available?)
• scientific article; zbMATH DE number 1942411 (Why is no real title available?)
• scientific article; zbMATH DE number 1759792 (Why is no real title available?)
• A New Mode of Encryption Providing a Tweakable Strong Pseudo-random Permutation
• Advances in Cryptology - CRYPTO 2003
• An Improved Security Bound for HCTR
• Automated Security Proofs with Sequences of Games
• Automated proofs of block cipher modes of operation
• Automated security proof for symmetric encryption modes
• Automated verification of block cipher modes of operation, an improved method
• Beyond provable security verifiable IND-CCA security of OAEP
• Computationally Sound Typing for Non-interference: The Case of Deterministic Encryption
• Computer-Aided Security Proofs for the Working Cryptographer
• Fast Software Encryption
• HCH: A New Tweakable Enciphering Scheme Using the Hash-Counter-Hash Approach
• Information Security
• Invertible Universal Hashing and the TET Encryption Mode
• On the equality of probabilistic terms
• Progress in Cryptology - INDOCRYPT 2004
• Progress in Cryptology - INDOCRYPT 2004
• The Security of the Extended Codebook (XCB) Mode of Operation
• The security of the cipher block chaining message authentication code
• Topics in Cryptology – CT-RSA 2004

Cited in

(6)

• Automated proofs of block cipher modes of operation
• Automated verification of block cipher modes of operation, an improved method
• Functional Correctness Proofs of Encryption Algorithms
• Automated security proof for symmetric encryption modes
• Assisted identification of mode of operation in binary code with dynamic data flow slicing
• Moving the bar on computationally sound exclusive-or

Describes a project that uses

Uses Software

• EasyCrypt

This page was built for publication: Automated proofs of block cipher modes of operation

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