cryspen / libcrux

The formally verified crypto library for Rust
https://cryspen.com/libcrux
Apache License 2.0
81 stars 13 forks source link

PQ-PSK prototype #310

Closed jschneider-bensch closed 3 months ago

jschneider-bensch commented 3 months ago

This crate implements a protocol for agreeing on a pre-shared key such that the protocol messages are secure against harvest-now-decrypt-later (HNDL) passive quantum attackers.

The protocol between initator A and receiver B roughly works as follows:

A:  (ik, enc) <- PQ-KEM(pk_B)
    K_0 <- KDF(ik, pk_B || enc || sctxt)
    K_m <- KDF(K_0, "Confirmation")
    K <- KDF(K_0, "PSK")
    mac_ttl <- MAC(K_m, psk_ttl)
A -> B: (enc, psk_ttl, mac_ttl)

Where

The crate implements the protocol based on several different internal KEMs: