6 results sorted by ID
Analysing the HPKE Standard
Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, Doreen Riepel
Public-key cryptography
The Hybrid Public Key Encryption (HPKE) scheme is an emerging standard currently under consideration by the Crypto Forum Research Group (CFRG) of the IETF as a candidate for formal approval. Of the four modes of HPKE, we analyse the authenticated mode HPKE_Auth in its single-shot encryption form as it contains what is, arguably, the most novel part of HPKE and has applications to other upcoming standards such as MLS.
HPKE_Auth’s intended application domain is captured by a new primitive...
An Analysis of Hybrid Public Key Encryption
Benjamin Lipp
Cryptographic protocols
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...
Automated Proof for Authorization Protocols of TPM 2.0 in Computational Model (full version)
Weijin Wang, Yu Qin, Dengguo Feng, Xiaobo Chu
Cryptographic protocols
We present the first automated proof of the authorization protocols in TPM 2.0 in the computational model. The Trusted Platform Module(TPM) is a chip that enables trust in computing platforms and achieves more security than software alone. The TPM interacts with a caller via a predefined set of commands. Many commands reference TPM-resident structures, and use of them may require authorization. The TPM will provide an acknowledgement once receiving an authorization. This interact ensure the...
Automatically Verified Mechanized Proof of One-Encryption Key Exchange
Bruno Blanchet
Cryptographic protocols
We present a mechanized proof of the password-based protocol One-Encryption Key Exchange (OEKE) using the computationally-sound protocol prover CryptoVerif. OEKE is a non-trivial protocol, and thus mechanizing its proof provides additional confidence that it is correct. This case study was also an opportunity to implement several important extensions of CryptoVerif, useful for proving many other protocols. We have indeed extended CryptoVerif to support the computational Diffie-Hellman...
Robust RFID Authentication Protocol with Formal Proof and Its Feasibility
Miyako Ohkubo, Shin'ichiro Matsuo, Yoshikazu Hanatani, Kazuo Sakiyama, Kazuo Ohta
The proloferation of RFID tags enhances everyday activities, such as by letting us reference the price, origin and circulation route of specific goods. On the other hand, this lecel of traceability gives rise to new privacy issues and the topic of developing cryptographic protocols for RFID- tags is garnering much attention. A large amount of research has been conducted in this area. In this paper, we reconsider the security model of RFID- authentication with a man-in-the-middle adversary...
Computationally Sound Mechanized Proofs of Correspondence Assertions
Bruno Blanchet
Cryptographic protocols
We present a new mechanized prover for showing correspondence
assertions for cryptographic protocols in the computational model.
Correspondence assertions are useful in particular for establishing
authentication.
Our technique produces proofs by sequences of games, as standard in
cryptography. These proofs are valid for a number of sessions
polynomial in the security parameter, in the presence of an active
adversary. Our technique can handle a wide variety of cryptographic
primitives,...
The Hybrid Public Key Encryption (HPKE) scheme is an emerging standard currently under consideration by the Crypto Forum Research Group (CFRG) of the IETF as a candidate for formal approval. Of the four modes of HPKE, we analyse the authenticated mode HPKE_Auth in its single-shot encryption form as it contains what is, arguably, the most novel part of HPKE and has applications to other upcoming standards such as MLS. HPKE_Auth’s intended application domain is captured by a new primitive...
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...
We present the first automated proof of the authorization protocols in TPM 2.0 in the computational model. The Trusted Platform Module(TPM) is a chip that enables trust in computing platforms and achieves more security than software alone. The TPM interacts with a caller via a predefined set of commands. Many commands reference TPM-resident structures, and use of them may require authorization. The TPM will provide an acknowledgement once receiving an authorization. This interact ensure the...
We present a mechanized proof of the password-based protocol One-Encryption Key Exchange (OEKE) using the computationally-sound protocol prover CryptoVerif. OEKE is a non-trivial protocol, and thus mechanizing its proof provides additional confidence that it is correct. This case study was also an opportunity to implement several important extensions of CryptoVerif, useful for proving many other protocols. We have indeed extended CryptoVerif to support the computational Diffie-Hellman...
The proloferation of RFID tags enhances everyday activities, such as by letting us reference the price, origin and circulation route of specific goods. On the other hand, this lecel of traceability gives rise to new privacy issues and the topic of developing cryptographic protocols for RFID- tags is garnering much attention. A large amount of research has been conducted in this area. In this paper, we reconsider the security model of RFID- authentication with a man-in-the-middle adversary...
We present a new mechanized prover for showing correspondence assertions for cryptographic protocols in the computational model. Correspondence assertions are useful in particular for establishing authentication. Our technique produces proofs by sequences of games, as standard in cryptography. These proofs are valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. Our technique can handle a wide variety of cryptographic primitives,...
