Title
Automated Analysis and Synthesis of Authenticated Encryption Schemes.
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.
Year
DOI
Venue
2015
10.1145/2810103.2813636
ACM Conference on Computer and Communications Security
DocType
Volume
Citations 
Journal
2015
9
PageRank 
References 
Authors
0.54
31
3
Name
Order
Citations
PageRank
Viet Tung Hoang146819.15
Jonathan Katz27579347.97
Alex J. Malozemoff31588.98