Join the talk here: https://aarhusuniversity.zoom.us/j/61235369353

Title: Hybrid Public Key Encryption: Mechanized Provable Security of a New IRTF Standard 

Abstract: Hybrid Public Key Encryption (HPKE) is a cryptographic primitive currently 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 encryption of arbitrary-sized plaintexts under a given recipient public key -- a widely-used technique long known under the name “hybrid encryption”. 

The new HPKE standardization effort stems from the desire to create an interoperable standard for use within the currently developed larger standards Encrypted Server Name Indication (ESNI) for TLS, and Messaging Layer Security (MLS). 

The development of HPKE is being accompanied by a formal cryptographic analysis using the CryptoVerif proof assistant, producing game- based proofs for message secrecy, key secrecy, and sender authentication for all HPKE modes. The analysis has motivated changes that have been incorporated into the standard, to improve its provable security.

In this talk we give an overview of HPKE, the mechanized proof effort, and the above mentioned changes. Finally, we give an insight into our current research project in which we develop a methodology to prove that an implementation adheres to the cryptographic theorems proved in CryptoVerif. Due to its simplicity, HPKE serves as first case study.

About the speaker: Benjamin Lipp is a second-year PhD student in the Prosecco research team at Inria Paris, under the supervision of Bruno Blanchet and Karthik Bhargavan.

About the talk: The talk is hosted by the Cryptography and Security Research Group at Aarhus University. The Aarhus Crypto Seminars are weekly seminar open to everyone with an interest in recent research in cryptology and information security. Further details about the research group and the weekly seminars can be found here: https://cs.au.dk/da/forskningsomraader/kryptografi-og-datasikkerhed/seminar/