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).

• Type: Conference
• Year: 2009
• Where: ASIAN
• Authors: Martin Gagné, Pascal Lafourcade, Yassine Lakhnech, Reihaneh Safavi-Naini
• Keywords: Algorithms, ASIAN 2009, Assertion Language, Encryption Modes, Semantic Security