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: ia.cr/2015/624
Discussion forum: Show discussion | Start new discussion
[ Cryptology ePrint archive ]