Sciweavers

Share
ASIAN
2009
Springer

Automated Security Proof for Symmetric Encryption Modes

10 years 3 months ago
Automated Security Proof for Symmetric Encryption Modes
Abstract. We presents a compositional Hoare logic for proving semantic security of modes of operation for symmetric key block ciphers. We propose a simple programming language to specify encryption modes and an assertion language that allows to state invariants and axioms and rules to establish such invariants. The assertion language consists of few atomic predicates. We were able to use our method to verify semantic security of several encryption modes including Cipher Block Chaining (CBC), Cipher Feedback mode (CFB), Output Feedback (OFB), and Counter mode (CTR).
Martin Gagné, Pascal Lafourcade, Yassine La
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2009
Where ASIAN
Authors Martin Gagné, Pascal Lafourcade, Yassine Lakhnech, Reihaneh Safavi-Naini
Comments (0)
books