Functional Correctness Proofs of Encryption Algorithms

DOI10.1007/11591191_36MaRDI QIDQ5387863zbMATH OpenOpenAlexFDO

Authors Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang

Publication date 27 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11591191_36

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automated security proof for symmetric encryption modes
• Automated proofs of block cipher modes of operation
• Computer-aided cryptographic proofs
• Automated proofs for asymmetric encryption
• Towards mechanized correctness proofs for cryptographic algorithms: axiomatization of a probabilistic Hoare style logic

Cited in

(3)

• Proof producing synthesis of arithmetic and cryptographic hardware
• Every bit counts: the binary representation of typed data and programs
• Automated security proof for symmetric encryption modes

Describes a project that uses

Uses Software

• AVISPA

This page was built for publication: Functional Correctness Proofs of Encryption Algorithms

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