Cryptology ePrint Archive: Report 2015/624

Automated Analysis and Synthesis of Authenticated Encryption Schemes

Viet Tung Hoang and Jonathan Katz and Alex J. Malozemoff

Abstract: Authenticated encryption (AE) schemes are symmetric-key encryption schemes ensuring strong notions of confidentiality and integrity. Although various AE schemes are known, there remains significant interest in developing schemes that are more efficient, meet even stronger security notions (e.g., misuse-resistance), or satisfy certain non-cryptographic properties (e.g., being patent-free).

We present an automated approach for analyzing and synthesizing blockcipher-based AE schemes, significantly extending prior work by Malozemoff et al. (CSF 2014) who synthesize encryption schemes satisfying confidentiality only. Our main insight is to restrict attention to a certain class of schemes that is expressive enough to capture several known constructions yet also admits automated reasoning about security. We use our approach to generate thousands of AE schemes with provable security guarantees, both known (e.g., variants of OCB and CCM) and new. Implementing two of these new schemes, we find their performance competitive with state-of-the-art AE schemes.

Category / Keywords: secret-key cryptography / authenticated encryption, synthesis

Original Publication (with major differences): ACM CCS 2015

Date: received 23 Jun 2015, last revised 11 Aug 2016

Contact author: tvhoang at engr ucsb edu

Available format(s): PDF | BibTeX Citation

Note: Letter instead of A4 paper size.

Version: 20160811:234504 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]