Paper 2015/624
Automated Analysis and Synthesis of Authenticated Encryption Schemes
Viet Tung Hoang, 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.
Note: Letter instead of A4 paper size.
Metadata
- Available format(s)
- Category
- Secret-key cryptography
- Publication info
- Published elsewhere. Major revision. ACM CCS 2015
- DOI
- 10.1145/2810103.2813636
- Keywords
- authenticated encryptionsynthesis
- Contact author(s)
- tvhoang @ engr ucsb edu
- History
- 2016-08-11: last of 3 revisions
- 2015-06-30: received
- See all versions
- Short URL
- https://ia.cr/2015/624
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2015/624, 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}, url = {https://eprint.iacr.org/2015/624} }