PQXDH in Lean

6.1. Protocol bundle🔗

Definition6.1
Group: PQXDH protocol definitions and roadmap from X3DH to full post-quantum security. (11)
Hover another entry in this group to preview it.
Preview
Definition 6.2
Blueprint label
  • pqxdh_verify_signatures
Group
  • PQXDH protocol definitions and roadmap from X3DH to full post-quantum security.
✓L∃∀Nused by 0

A PQXDH bundle packages all public values that Bob publishes to the server: identity key, signed pre-key, one-time pre-key, post-quantum signed pre-key, and associated signatures. Signature verification is included as a method.

Code for Definition6.1●1 definition
  • structure PQXDHBundle.{u_1, u_2, u_3} (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (PK_kemType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (S_sigType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1] : Type (max (max u_1 u_2) u_3)A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. 
    structure PQXDHBundle.{u_1, u_2, u_3} (GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (PK_kemType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ) (S_sigType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1] :
  Type (max (max u_1 u_2) u_3)A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. 
    §2.3, p. 472 and Figure 1, p. 471: Bob's prekey bundle including the
post-quantum KEM public key and signatures authenticating the signed prekeys.
"In the initial message to Alex, Blake includes PQSPKᵦᵖᵏ and
sign(PQSPKᵦᵖᵏ, IKᵦˢᵏ)." (§2.3, item 2, p. 472)

    Constructor

    PQXDHBundle.mk.{u_1, u_2, u_3}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {PK_kemType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {S_sigType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1]
  (IKᵦG SPKᵦG : GType u_1) (sig_spkS_sig : S_sigType u_3)
  (OPKᵦG : GType u_1) (PQSPKPK_kem : PK_kemType u_2)
  (sig_pqspkS_sig : S_sigType u_3) :
  PQXDHBundlePQXDHBundle.{u_1, u_2, u_3} (G : Type u_1) (PK_kem : Type u_2) (S_sig : Type u_3) [AddCommGroup G] :
  Type (max (max u_1 u_2) u_3)§2.3, p. 472 and Figure 1, p. 471: Bob's prekey bundle including the
post-quantum KEM public key and signatures authenticating the signed prekeys.
"In the initial message to Alex, Blake includes PQSPKᵦᵖᵏ and
sign(PQSPKᵦᵖᵏ, IKᵦˢᵏ)." (§2.3, item 2, p. 472)  GType u_1 PK_kemType u_2 S_sigType u_3

    Fields

    IKᵦG : GType u_1
    SPKᵦG : GType u_1
    sig_spkS_sig : S_sigType u_3
    OPKᵦG : GType u_1
    PQSPKPK_kem : PK_kemType u_2
    sig_pqspkS_sig : S_sigType u_3
    complete
Definition6.2
Group: PQXDH protocol definitions and roadmap from X3DH to full post-quantum security. (11)
Hover another entry in this group to preview it.
Preview
Definition 6.1
Blueprint label
  • pqxdh_bundle
Group
  • PQXDH protocol definitions and roadmap from X3DH to full post-quantum security.
✓L∃∀Nused by 0

Alice verifies both bundle signatures (SPK and PQSPK) under Bob's identity public key before proceeding. Returns true iff both signatures are valid (Figure 1).

Code for Definition6.2●1 definition
  • def PQXDHBundle.verify_signatures.{u_1, u_2, u_3, u_4, u_5, u_6}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1] {PK_sigType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {SK_sigType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {MType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {S_sigType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {PK_kemType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } (bundlePQXDHBundle G PK_kem S_sig : PQXDHBundlePQXDHBundle.{u_1, u_2, u_3} (G : Type u_1) (PK_kem : Type u_2) (S_sig : Type u_3) [AddCommGroup G] :
  Type (max (max u_1 u_2) u_3)§2.3, p. 472 and Figure 1, p. 471: Bob's prekey bundle including the
post-quantum KEM public key and signatures authenticating the signed prekeys.
"In the initial message to Alex, Blake includes PQSPKᵦᵖᵏ and
sign(PQSPKᵦᵖᵏ, IKᵦˢᵏ)." (§2.3, item 2, p. 472)  GType u_1 PK_kemType u_6 S_sigType u_5)
  (sig_schemeSig PK_sig SK_sig M S_sig : SigSig.{u_1, u_2, u_3, u_4} (PK_sig : Type u_1) (SK_sig : Type u_2) (M : Type u_3) (S : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)§2.5, p. 472 assumption 2 and Figure 1, p. 471: Abstract digital signature
scheme. The paper uses "the signature Sig (XEdDSA), is EUF-CMA" (§2.5, p. 472).
In Figure 1, Alice verifies "sign(SPKᵦᵖᵏ, IKᵦˢᵏ), sign(PQSPKᵦᵖᵏ, IKᵦˢᵏ)".
Correctness requires that honestly generated signatures verify under the matching
public key. Concrete instantiation: XEdDSA over Curve25519.  PK_sigType u_2 SK_sigType u_3 MType u_4 S_sigType u_5) (IKᵦ_sigPK_sig : PK_sigType u_2)
  (encode_spkG → M : GType u_1 → MType u_4) (encode_pqspkPK_kem → M : PK_kemType u_6 → MType u_4) : BoolBool : TypeThe Boolean values, `true` and `false`.

Logically speaking, this is equivalent to `Prop` (the type of propositions). The distinction is
public important for programming: both propositions and their proofs are erased in the code generator,
while `Bool` corresponds to the Boolean type in most programming languages and carries precisely one
bit of run-time information.

    def PQXDHBundle.verify_signatures.{u_1, u_2,
    u_3, u_4, u_5, u_6}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  GType u_1]
  {PK_sigType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {SK_sigType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {MType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {S_sigType u_5 : Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {PK_kemType u_6 : Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  (bundlePQXDHBundle G PK_kem S_sig : PQXDHBundlePQXDHBundle.{u_1, u_2, u_3} (G : Type u_1) (PK_kem : Type u_2) (S_sig : Type u_3) [AddCommGroup G] :
  Type (max (max u_1 u_2) u_3)§2.3, p. 472 and Figure 1, p. 471: Bob's prekey bundle including the
post-quantum KEM public key and signatures authenticating the signed prekeys.
"In the initial message to Alex, Blake includes PQSPKᵦᵖᵏ and
sign(PQSPKᵦᵖᵏ, IKᵦˢᵏ)." (§2.3, item 2, p. 472)  GType u_1 PK_kemType u_6 S_sigType u_5)
  (sig_schemeSig PK_sig SK_sig M S_sig : SigSig.{u_1, u_2, u_3, u_4} (PK_sig : Type u_1) (SK_sig : Type u_2) (M : Type u_3) (S : Type u_4) :
  Type (max (max (max u_1 u_2) u_3) u_4)§2.5, p. 472 assumption 2 and Figure 1, p. 471: Abstract digital signature
scheme. The paper uses "the signature Sig (XEdDSA), is EUF-CMA" (§2.5, p. 472).
In Figure 1, Alice verifies "sign(SPKᵦᵖᵏ, IKᵦˢᵏ), sign(PQSPKᵦᵖᵏ, IKᵦˢᵏ)".
Correctness requires that honestly generated signatures verify under the matching
public key. Concrete instantiation: XEdDSA over Curve25519.  PK_sigType u_2 SK_sigType u_3 MType u_4 S_sigType u_5)
  (IKᵦ_sigPK_sig : PK_sigType u_2) (encode_spkG → M : GType u_1 → MType u_4)
  (encode_pqspkPK_kem → M : PK_kemType u_6 → MType u_4) : BoolBool : TypeThe Boolean values, `true` and `false`.

Logically speaking, this is equivalent to `Prop` (the type of propositions). The distinction is
public important for programming: both propositions and their proofs are erased in the code generator,
while `Bool` corresponds to the Boolean type in most programming languages and carries precisely one
bit of run-time information.

    Figure 1, p. 471 "Verify signatures": Alice verifies Bob's bundle
signatures before proceeding. Returns `true` iff both the SPK signature
and the PQSPK signature are valid under Bob's identity public key.
    complete