Cryptology ePrint Archive: Report 2020/243

An Analysis of Hybrid Public Key Encryption

Benjamin Lipp

Abstract: Hybrid Public Key Encryption (HPKE) is a cryptographic primitive being standardized by the Crypto Forum Research Group (CFRG) within the Internet Research Task Force (IRTF). HPKE schemes combine asymmetric and symmetric cryptographic primitives for efficient authenticated encryption of arbitrary-sized plaintexts under a given recipient public key. This document presents a mechanized cryptographic analysis done with CryptoVerif, of all four HPKE modes, instantiated with a prime-order-group Diffie-Hellman Key Encapsulation Mechanism (KEM).

Category / Keywords: cryptographic protocols / public-key cryptography, hybrid encryption, formal verification, CryptoVerif

Date: received 23 Feb 2020, last revised 23 Feb 2020

Contact author: benjamin lipp at inria fr

Available format(s): PDF | BibTeX Citation

Version: 20200225:203507 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]