Paper 2015/624

Automated Analysis and Synthesis of Authenticated Encryption Schemes

Viet Tung Hoang, Jonathan Katz, and Alex J. Malozemoff


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.

Note: Letter instead of A4 paper size.

Available format(s)
Secret-key cryptography
Publication info
Published elsewhere. Major revision. ACM CCS 2015
authenticated encryptionsynthesis
Contact author(s)
tvhoang @ engr ucsb edu
2016-08-11: last of 3 revisions
2015-06-30: received
See all versions
Short URL
Creative Commons Attribution


      author = {Viet Tung Hoang and Jonathan Katz and Alex J.  Malozemoff},
      title = {Automated Analysis and Synthesis of Authenticated Encryption Schemes},
      howpublished = {Cryptology ePrint Archive, Paper 2015/624},
      year = {2015},
      doi = {10.1145/2810103.2813636},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.