This paper at Springer https://link.springer.com/chapter/10.1007/978-3-030-77870-5_4.
HPKE_Auth's intended application domain is captured by a new primitive which we call Authenticated Public Key Encryption (APKE). We provide syntax and security definitions for APKE schemes, as well as for the related Authenticated Key Encapsulation Mechanisms (AKEMs). We prove security of the AKEM scheme DH-AKEM underlying HPKE_Auth based on the Gap Diffie-Hellman assumption and provide general AKEM/DEM composition theorems with which to argue about HPKE_Auth's security. To this end, we also formally analyse HPKE_Auth's key schedule and key derivation functions. To increase confidence in our results we use the automatic theorem proving tool CryptoVerif. All our bounds are quantitative and we discuss their practical implications for HPKE_Auth.
As an independent contribution we propose the new framework of nominal groups that allows us to capture abstract syntactical and security properties of practical elliptic curves, including the Curve25519 and Curve448 based groups (which do not constitute cyclic groups).
@INPROCEEDINGS{AlwenetalEurocrypt21,
AUTHOR = {Joël Alwen and Bruno Blanchet and Eduard Hauck and Eike Kiltz and Benjamin Lipp and Doreen Riepel},
TITLE = {Analysing the {HPKE} Standard},
BOOKTITLE = {Eurocrypt 2021},
YEAR = {2021},
EDITOR = {Anne Canteaut and Francois-Xavier Standaert},
VOLUME = {12696},
SERIES = {Lecture Notes in Computer Science},
PAGES = {87--116},
MONTH = OCT,
ADDRESS = {Zagreb, Croatia},
PUBLISHER = {Springer}
}