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 Lin | 1 | 23 | 2.96 |
Christopher Lynch | 2 | 27 | 3.62 |