Title
Formal Analysis of Symbolic Authenticity
Abstract
Authenticated encryption schemes are ways of encrypting messages which simultaneously assure the secrecy and authenticity of data. Designing authenticated encryption schemes can be error-prone. In this paper, we consider the authenticity of authenticated encryption schemes. We introduce the notion of symbolic authenticity, and present two inference systems for verifying symbolic authenticity. The first inference system works for authenticated encryption schemes for messages of fixed length. It is sound, complete and terminating. The second one works for authenticated encryption schemes for messages of arbitrary length. It is sound, terminating, and complete under some condition. These inference systems can be used to automatically synthesize authenticated encryption schemes.
Year
DOI
Venue
2021
10.1007/978-3-030-86205-3_15
FRONTIERS OF COMBINING SYSTEMS (FROCOS 2021)
Keywords
DocType
Volume
Unification, Authenticated encryption, Formal methods
Conference
12941
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
0
2
Name
Order
Citations
PageRank
Hai Lin1232.96
Christopher Lynch2273.62