Welcome to the resource topic for 2023/1753
Title:
Formal verification of the post-quantum security properties of IKEv2 PPK (RFC 8784) using the Tamarin Prover
Authors: Sophie Stevens
Abstract:The Internet Key Exchange version 2 (IKEv2) (RFC 7296) is a component of IPsec used to authenticate two parties (the initiator and responder) to each other and to establish a set of security parameters for the communications. The security parameters include secret keys to encrypt and authenticate data as well as the negotiation of a set of cryptographic algorithms. The core documentation uses exclusively Diffie-Hellman exchanges to agree the security information. However, this is not a quantum-secure option due to the ability of Shor’s algorithm to break the security assumption underlying the Diffie-Hellman. A post-quantum solution is to include a preshared key in the exchange, as proposed by the extension RFC 8784; assuming that this preshared key has sufficient entropy, the keys created in the IKEv2 exchange will be resistant to a quantum computer. In this paper, we investigate the security claims of RFC 8784 using formal verification methods. We find that keys created using the preshared key are secret from an adversary. However, certain authentication properties of the protocol that are weakened under the assumption that Diffie-Hellman is insecure are not recovered using the preshared key.
ePrint: https://eprint.iacr.org/2023/1753
See all topics related to this paper.
Feel free to post resources that are related to this paper below.
Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.
For more information, see the rules for Resource Topics .