PQXDH.lean
Declarations on this page (61)
- class HasExecBytes
- inductive KeyKind
- structure PQXDHState
- structure HandshakeKeys
- inductive PQXDHEvent
-
def KeyKind.
ofBits -
def KeyKind.
toBits - instance L144
- class HasExecTrace
- def pqxdhLabel
- def discontinuity
- def ecKeyType
- def kemKeyType
- def encodeEC
- def encodeKEM
- def serializedIk
- def pqxdhIkm
- def pqxdhKdf
- def aliceAgreement
- def errToOption
- def bobAgreement
- def extractDhSecretKey
- def isRegisteredB
- def opkUsedB
- def brokenDHB
- def brokenKEMB
- def getKey
- def registerIdentity
- def registerCorruptIdentity
- def lookupIdentity
- def genSignedPrekey
- def genPQPrekey
- def genOneTimePrekey
- structure BundleHandles
- structure AliceHandshakeOut
- def aliceHandshake
- structure BobKeyHandles
- structure BobHandshakeOut
- def bobHandshake
- structure PreKeyMsgHandles
- def compromiseIK
- def compromiseSPK
- def compromisePQSPK
- def compromiseOPK
- def breakDH
- def breakKEM
- def invertDH
- def invertKEM
-
def registerIdentity.
reachability -
def registerCorruptIdentity.
reachability -
def genSignedPrekey.
reachability -
def genPQPrekey.
reachability -
def genOneTimePrekey.
reachability -
def compromiseIK.
reachability -
def compromiseSPK.
reachability -
def compromisePQSPK.
reachability -
def compromiseOPK.
reachability -
def breakDH.
reachability -
def breakKEM.
reachability -
def invertDH.
reachability -
def invertKEM.
reachability
Symbolic PQXDH Handshake, PKI, Prekeys, and Threat Model
DyLean model of libsignal's PQXDH key schedule, authentic PKI registration, prekey publication, trace-silent handshake subroutines (aliceHandshake, bobHandshake), and key-compromise / primitive-break transitions. Role names follow libsignal (AliceDone fetches a bundle; BobDone publishes prekeys).
namespace DY.Libsignal.PQXDHopen DY.Comparseexport DY.X25519 (x25519LowOrder isCanonicalKey agree)export DY.Libsignal.TripleRatchet (MessageKeys SignalMsg lit litByte hmac hkdfBlock1 hkdfBlock2
hkdfBlock3 zeroSalt messageVersion maxForwardJumps u32Max
anyEventOnTrace guardTrace getStoredLocalStateAt?)public section ExecBytesConfigclass HasExecBytes
class HasExecBytes where
[bytesFunc: BytesFunctor]
[bytesFunc0: BytesFunctor.Has Random.SubF]
[bytesFunc1: BytesFunctor.Has Literal.SubF]
[bytesFunc2: BytesFunctor.Has Concat.SubF]
[bytesFunc3: BytesFunctor.Has DiffieHellman.SubF]
[bytesFunc4: BytesFunctor.Has KdfExtract.SubF]
[bytesFunc8: BytesFunctor.Has X25519.SubF]
[bytesFuncKem: BytesFunctor.Has PQKem.SubF]
[bytesFuncSig: BytesFunctor.Has Signature.SubF]
[bytesLen: BytesLength]
[bytesLen0: BytesLength.Has Random.SubF.length]
[bytesLen1: BytesLength.Has Literal.SubF.length]
[bytesLen2: BytesLength.Has Concat.SubF.length]
[bytesLen3: BytesLength.Has DiffieHellman.SubF.length]
[bytesLen4: BytesLength.Has KdfExtract.SubF.length]
[bytesLen8: BytesLength.Has X25519.SubF.length]
[bytesLenKem: BytesLength.Has PQKem.SubF.length]
[bytesLenSig: BytesLength.Has Signature.SubF.length]
[att: AttackerKnowledge]
[att0: AttackerKnowledge.Has Random.attackerKnowledge]
[att1: AttackerKnowledge.Has Literal.attackerKnowledge]
[att2: AttackerKnowledge.Has Concat.attackerKnowledge]
[att3: AttackerKnowledge.Has DiffieHellman.attackerKnowledge]
[att4: AttackerKnowledge.Has KdfExtract.attackerKnowledge]
[att8: AttackerKnowledge.Has X25519.attackerKnowledge]
[attKem: AttackerKnowledge.Has PQKem.attackerKnowledge]
[attSig: AttackerKnowledge.Has Signature.attackerKnowledge]inductive KeyKind
Tag distinguishing stored long-term and prekey secrets in PQXDHState.
inductive KeyKind where
| identity
| signedPrekey
| pqPrekey
| oneTimePrekey
deriving DecidableEqstructure PQXDHState
Stored secret key of a participant (identity, signed prekey, Kyber prekey, or one-time prekey). Alice's ephemeral base key is dropped after pqxdh_initiate and never stored.
structure PQXDHState where
kind: KeyKind
sk: Bytesstructure HandshakeKeys
Output of HandshakeKeys::derive: 32-byte root key, initial chain key, and initial SPQR key.
structure HandshakeKeys where
rk: Bytes
ck: Bytes
pqr: Bytesinductive PQXDHEvent
Protocol and threat events logged by PQXDH transitions (carrying public keys so events do not reveal secrets).
inductive PQXDHEvent where
| IdentityRegistered (p: Participant) (ikPk vk: Bytes) (honest: Bool)
| SignedPrekeyPublished (b: Participant) (spkPk: Bytes)
| PQPrekeyPublished (b: Participant) (pqPk: Bytes)
| OneTimePrekeyPublished (b: Participant) (opkPk: Bytes)
| AliceDone (a b: Participant) (ikA ikB spk pqpk: Bytes) (opk: Option Bytes) (ek ct: Bytes)
(keys: HandshakeKeys)
| BobDone (b a: Participant) (ikB ikA spk pqpk: Bytes) (opk: Option Bytes) (ek ct: Bytes)
(keys: HandshakeKeys)
| CompromisedIK (p: Participant) (ikPk: Bytes)
| CompromisedSPK (b: Participant) (spkPk: Bytes)
| CompromisedPQSPK (b: Participant) (pqPk: Bytes)
| CompromisedOPK (b: Participant) (opkPk: Bytes)
| BrokenDH
| BrokenKEM
/-- Ghost event recording single-use consumption of one-time prekey `opkPk` by `b`. -/
| OPKUsed (b: Participant) (opkPk: Bytes)
def KeyKind.
def KeyKind.ofBits: Bool × Bool → KeyKind
| (false, false) => .identity
| (false, true) => .signedPrekey
| (true, false) => .pqPrekey
| (true, true) => .oneTimePrekey
def KeyKind.
@[expose] def KeyKind.toBits: KeyKind → Bool × Bool
| .identity => (false, false)
| .signedPrekey => (false, true)
| .pqPrekey => (true, false)
| .oneTimePrekey => (true, true)instance
public
instance: ParseableSerializeable PQXDHState := .make <|
.triviallyIsomorphic
(.prod .bool (.prod .bool .bytes))
(fun (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk })
(fun { kind, sk } => (kind.toBits.1, kind.toBits.2, sk))
(inst✝:HasExecBytes⊢ Function.LeftInverse
(fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk } inst✝:HasExecBytesb1:Boolb2:Boolsk:Bytes⊢ (fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
((fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
(b1, b2, sk)) =
(b1, b2, sk); inst✝:HasExecBytesb2:Boolsk:Bytes⊢ (fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
((fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
(false, b2, sk)) =
(false, b2, sk)inst✝:HasExecBytesb2:Boolsk:Bytes⊢ (fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
((fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
(true, b2, sk)) =
(true, b2, sk) inst✝:HasExecBytesb2:Boolsk:Bytes⊢ (fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
((fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
(false, b2, sk)) =
(false, b2, sk)inst✝:HasExecBytesb2:Boolsk:Bytes⊢ (fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
((fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
(true, b2, sk)) =
(true, b2, sk) inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
((fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
(true, false, sk)) =
(true, false, sk)inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
((fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
(true, true, sk)) =
(true, true, sk) inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
((fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
(false, false, sk)) =
(false, false, sk)inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
((fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
(false, true, sk)) =
(false, true, sk)inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
((fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
(true, false, sk)) =
(true, false, sk)inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
((fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
(true, true, sk)) =
(true, true, sk) All goals completed! 🐙)
(inst✝:HasExecBytes⊢ Function.RightInverse
(fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk } inst✝:HasExecByteskind:KeyKindsk:Bytes⊢ (fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
((fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
{ kind := kind, sk := sk }) =
{ kind := kind, sk := sk }; inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
((fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
{ kind := KeyKind.identity, sk := sk }) =
{ kind := KeyKind.identity, sk := sk }inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
((fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
{ kind := KeyKind.signedPrekey, sk := sk }) =
{ kind := KeyKind.signedPrekey, sk := sk }inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
((fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
{ kind := KeyKind.pqPrekey, sk := sk }) =
{ kind := KeyKind.pqPrekey, sk := sk }inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
((fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
{ kind := KeyKind.oneTimePrekey, sk := sk }) =
{ kind := KeyKind.oneTimePrekey, sk := sk } inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
((fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
{ kind := KeyKind.identity, sk := sk }) =
{ kind := KeyKind.identity, sk := sk }inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
((fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
{ kind := KeyKind.signedPrekey, sk := sk }) =
{ kind := KeyKind.signedPrekey, sk := sk }inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
((fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
{ kind := KeyKind.pqPrekey, sk := sk }) =
{ kind := KeyKind.pqPrekey, sk := sk }inst✝:HasExecBytessk:Bytes⊢ (fun x =>
match x with
| (b1, b2, sk) => { kind := KeyKind.ofBits (b1, b2), sk := sk })
((fun x =>
match x with
| { kind := kind, sk := sk } => (kind.toBits.fst, kind.toBits.snd, sk))
{ kind := KeyKind.oneTimePrekey, sk := sk }) =
{ kind := KeyKind.oneTimePrekey, sk := sk } All goals completed! 🐙)end Formatspublic section ExecTraceConfigclass HasExecTrace
class HasExecTrace extends toPQXDHExecBytes : HasExecBytes where
[traceExec: ExecTraceTypes]
[traceExec0: ExecTraceTypes.Has Network.ExecEntryT]
[traceExec1: ExecTraceTypes.Has Random.ExecEntryT]
[traceExec2: ExecTraceTypes.Has (ProtocolEvent.ExecEntryT PQXDHEvent)]
[traceExec3: ExecTraceTypes.Has (PersistentLocalState.CompromisableState.ExecEntryT PQXDHState)]
[attBase: BaseAttackerKnowledge]end ExecTraceConfig@[expose] public section KeySchedulevariable [HasExecBytes]open Literal Concat DiffieHellman KdfExtract PQKemdef pqxdhLabel
HKDF info string of HandshakeKeys::derive.
def pqxdhLabel: Bytes := lit "WhisperText_X25519_SHA-256_CRYSTALS-KYBER-1024"def discontinuity
32-byte 0xFF domain-separation prefix of the PQXDH input key material.
def discontinuity: Bytes := literalToBytes ⟨Array.replicate 32 0xFF⟩def ecKeyType
KeyType::Djb (0x05) prefix byte for serialized X25519 public keys.
def ecKeyType: UInt8 := 0x05def kemKeyType
kem::KeyType::Kyber1024 (0x08) prefix byte for serialized Kyber-1024 public keys.
def kemKeyType: UInt8 := 0x08def encodeEC
PublicKey::serialize for X25519 (0x05 || pk).
def encodeKEM
kem::PublicKey::serialize for Kyber-1024 (0x08 || pk).
def encodeKEM (pk: Bytes): Bytes := concat (litByte kemKeyType) pkdef serializedIk
def serializedIk (ikPk: Bytes): Bytes := encodeEC ikPkdef pqxdhIkm
Concatenated PQXDH secret input: discontinuity || dh1 || dh2 || dh3 [|| dh4] || ss.
def pqxdhIkm (dh1 dh2 dh3: Bytes) (dh4: Option Bytes) (ss: Bytes): Bytes :=
concat discontinuity (concat dh1 (concat dh2 (concat dh3
(match dh4 with
| some d => concat d ss
| none => ss))))def pqxdhKdf
HandshakeKeys::derive: HKDF-SHA256 with zeroSalt and pqxdhLabel into (rk, ck, pqr).
def pqxdhKdf (ikm: Bytes): HandshakeKeys :=
let prk := hmac zeroSalt ikm
{ rk := hkdfBlock1 prk pqxdhLabel
ck := hkdfBlock2 prk pqxdhLabel
pqr := hkdfBlock3 prk pqxdhLabel }def aliceAgreement
pqxdh_initiate: encapsulates to pqPk under entropy and derives (ct, HandshakeKeys).
def errToOption
def errToOption {α: Type} (x: Err α): Option α := xdef bobAgreement
pqxdh_accept: decapsulates ct under pqsk (with implicit rejection kemRejKey pqsk ct on decapsulation failure) and derives HandshakeKeys.
def bobAgreement (ikB spk pqsk: Bytes) (opk: Option Bytes) (ikAPk ekPk ct: Bytes):
Option HandshakeKeys := do
let ss := (errToOption (kemDecap pqsk ct)).getD (kemRejKey pqsk ct)
pure (pqxdhKdf (pqxdhIkm (agree ikAPk spk) (agree ekPk ikB) (agree ekPk spk)
(opk.map (agree ekPk ·)) ss))def extractDhSecretKey
Discrete-log extraction of sk from dhPk sk.
def extractDhSecretKey (pk: Bytes): Option Bytes :=
match pk.view? DiffieHellman.DhPk.SubF with
| some { sk } => some sk
| none => noneend KeySchedule@[expose] public section Specificationvariable [HasExecTrace]open DiffieHellman Signature PQKemopen PersistentLocalState (getLocalState storeLocalState)open Network (sendMessage receiveMessage)open Random (genRand)open ProtocolEvent (logEvent)def isRegisteredB
def isRegisteredB (tr: ExecTrace) (p: Participant) : Bool :=
anyEventOnTrace PQXDHEvent tr fun
| .IdentityRegistered p' _ _ _ => p' == p
| _ => falsedef opkUsedB
def opkUsedB (tr: ExecTrace) (b: Participant) (opkPk: Bytes) : Bool :=
anyEventOnTrace PQXDHEvent tr fun
| .OPKUsed b' o => b' == b && o == opkPk
| _ => falsedef brokenDHB
def brokenDHB (tr: ExecTrace) : Bool :=
anyEventOnTrace PQXDHEvent tr fun | .BrokenDH => true | _ => falsedef brokenKEMB
def brokenKEMB (tr: ExecTrace) : Bool :=
anyEventOnTrace PQXDHEvent tr fun | .BrokenKEM => true | _ => falsedef getKey
def getKey (p: Participant) (stateIdx: Nat) (kind: KeyKind) : Traceful Bytes := do
let st: PQXDHState ← getLocalState p stateIdx
guard (st.kind = kind)
pure st.skdef registerIdentity
Register an honest identity for p (at most once per participant): draws ik, publishes dhPk ik and its XEdDSA verification key vk ik, logs IdentityRegistered p (dhPk ik) (vk ik) true, and stores ik in the modeled authentic PKI.
def registerIdentity (p: Participant) : Traceful Nat := do
guardTrace fun tr => !isRegisteredB tr p
let ik ← genRand 32
logEvent (PQXDHEvent.IdentityRegistered p (dhPk ik) (vk ik) true)
let _ ← sendMessage (dhPk ik)
let _ ← sendMessage (vk ik)
storeLocalState p { kind := .identity, sk := ik : PQXDHState }def registerCorruptIdentity
Register an attacker-controlled identity for p from network handle skIdx (at most once per participant), logging IdentityRegistered ... false and CompromisedIK.
def registerCorruptIdentity (p: Participant) (skIdx: Nat) : Traceful Unit := do
guardTrace fun tr => !isRegisteredB tr p
let ik ← receiveMessage skIdx
logEvent (PQXDHEvent.IdentityRegistered p (dhPk ik) (vk ik) false)
logEvent (PQXDHEvent.CompromisedIK p (dhPk ik))def lookupIdentity
Look up (ikPk, vkPk) for p from the IdentityRegistered event at regIdx.
def lookupIdentity (p: Participant) (regIdx: Nat) : Traceful (Bytes × Bytes) := do
let e: ProtocolEvent.ExecEntryT PQXDHEvent ← getEntry regIdx
let .IdentityRegistered p' ikPk vkPk _ := e.ev | failure
guard (p' = p)
pure (ikPk, vkPk)def genSignedPrekey
Generate, sign (encodeEC), store, and publish an X25519 signed prekey for b.
def genSignedPrekey (b: Participant) (idStateIdx: Nat) : Traceful Nat := do
let ik ← getKey b idStateIdx .identity
let spk ← genRand 32
let nonce ← genRand 64
logEvent (PQXDHEvent.SignedPrekeyPublished b (dhPk spk))
let h ← storeLocalState b { kind := .signedPrekey, sk := spk : PQXDHState }
let _ ← sendMessage (dhPk spk)
let _ ← sendMessage (sign ik nonce (encodeEC (dhPk spk)))
pure hdef genPQPrekey
Generate, sign (encodeKEM), store, and publish a reusable Kyber-1024 prekey for b.
def genPQPrekey (b: Participant) (idStateIdx: Nat) : Traceful Nat := do
let ik ← getKey b idStateIdx .identity
let pqsk ← genRand 64
let nonce ← genRand 64
logEvent (PQXDHEvent.PQPrekeyPublished b (kemPk pqsk))
let h ← storeLocalState b { kind := .pqPrekey, sk := pqsk : PQXDHState }
let _ ← sendMessage (kemPk pqsk)
let _ ← sendMessage (sign ik nonce (encodeKEM (kemPk pqsk)))
pure hdef genOneTimePrekey
Generate, store, and publish an unsigned X25519 one-time prekey for b.
def genOneTimePrekey (b: Participant) : Traceful Nat := do
let opk ← genRand 32
logEvent (PQXDHEvent.OneTimePrekeyPublished b (dhPk opk))
let h ← storeLocalState b { kind := .oneTimePrekey, sk := opk : PQXDHState }
let _ ← sendMessage (dhPk opk)
pure hstructure BundleHandles
Network handles for a received prekey bundle.
structure BundleHandles where
spk: Nat
spkSig: Nat
pqpk: Nat
pqpkSig: Nat
opk: Option Natstructure AliceHandshakeOut
structure AliceHandshakeOut where
ikA: Bytes
ikB: Bytes
spk: Bytes
pqpk: Bytes
opk: Option Bytes
ek: Bytes
ct: Bytes
keys: HandshakeKeysdef aliceHandshake
Alice's handshake subroutine (process_prekey_bundle / pqxdh_initiate): verifies both prekey signatures under b's PKI verification key, draws ephemeral secret ek, rejects low-order prekeys, encapsulates, and derives HandshakeKeys without logging events or storing state.
def aliceHandshake (a b: Participant) (idStateIdx regIdxB: Nat) (h: BundleHandles) :
Traceful AliceHandshakeOut := do
let ikA ← getKey a idStateIdx .identity
let (ikB, vkB) ← lookupIdentity b regIdxB
let spk ← receiveMessage h.spk
let spkSig ← receiveMessage h.spkSig
let pqpk ← receiveMessage h.pqpk
let pqpkSig ← receiveMessage h.pqpkSig
guard (verify vkB (encodeEC spk) spkSig)
guard (verify vkB (encodeKEM pqpk) pqpkSig)
let opk ← match h.opk with
| some i => do pure (some (← receiveMessage i))
| none => pure none
let ek ← genRand 32
guard (!x25519LowOrder spk)
guard (opk.all fun o => !x25519LowOrder o)
let entropy ← genRand 32
let (ct, keys) := aliceAgreement ikA ek ikB spk pqpk opk entropy
pure { ikA := dhPk ikA, ikB, spk, pqpk, opk, ek := dhPk ek, ct, keys }structure BobKeyHandles
Local state handles for Bob's secrets in bobHandshake.
structure BobKeyHandles where
ik: Nat
spk: Nat
pqspk: Nat
opk: Option Natstructure BobHandshakeOut
structure BobHandshakeOut where
ikB: Bytes
ikA: Bytes
spk: Bytes
pqpk: Bytes
opk: Option Bytes
ek: Bytes
ct: Bytes
spkSk: Bytes
keys: HandshakeKeysdef bobHandshake
Bob's handshake subroutine (process_prekey_impl / pqxdh_accept): loads Bob's secrets and Alice's PKI identity key, checks isCanonicalKey ek, and derives HandshakeKeys without logging events or storing state.
def bobHandshake (b a: Participant) (h: BobKeyHandles) (regIdxA ekIdx ctIdx: Nat) :
Traceful BobHandshakeOut := do
let ikB ← getKey b h.ik .identity
let spkSk ← getKey b h.spk .signedPrekey
let pqsk ← getKey b h.pqspk .pqPrekey
let opkSk ← match h.opk with
| some i => do pure (some (← getKey b i .oneTimePrekey))
| none => pure none
let (ikA, _) ← lookupIdentity a regIdxA
let ek ← receiveMessage ekIdx
let ct ← receiveMessage ctIdx
guard (isCanonicalKey ek)
let some keys := bobAgreement ikB spkSk pqsk opkSk ikA ek ct | failure
pure { ikB := dhPk ikB, ikA, spk := dhPk spkSk, pqpk := kemPk pqsk, opk := opkSk.map dhPk,
ek, ct, spkSk, keys }structure PreKeyMsgHandles
Network handles for an incoming PreKeySignalMessage (ek, ct, and inner SignalMessage).
structure PreKeyMsgHandles where
ek: Nat
ct: Nat
msg: Natdef compromiseIK
def compromiseIK (p: Participant) (stateIdx: Nat) : Traceful Nat := do
let ik ← getKey p stateIdx .identity
logEvent (PQXDHEvent.CompromisedIK p (dhPk ik))
sendMessage ikdef compromiseSPK
def compromiseSPK (b: Participant) (stateIdx: Nat) : Traceful Nat := do
let spk ← getKey b stateIdx .signedPrekey
logEvent (PQXDHEvent.CompromisedSPK b (dhPk spk))
sendMessage spkdef compromisePQSPK
def compromisePQSPK (b: Participant) (stateIdx: Nat) : Traceful Nat := do
let pqsk ← getKey b stateIdx .pqPrekey
logEvent (PQXDHEvent.CompromisedPQSPK b (kemPk pqsk))
sendMessage pqskdef compromiseOPK
Leak an unconsumed one-time prekey secret of b.
def compromiseOPK (b: Participant) (stateIdx: Nat) : Traceful Nat := do
let opk ← getKey b stateIdx .oneTimePrekey
guardTrace fun tr => !opkUsedB tr b (dhPk opk)
logEvent (PQXDHEvent.CompromisedOPK b (dhPk opk))
sendMessage opkdef breakDH
def breakDH : Traceful Unit := logEvent PQXDHEvent.BrokenDHdef breakKEM
def breakKEM : Traceful Unit := logEvent PQXDHEvent.BrokenKEMdef invertDH
Discrete-log oracle enabled after BrokenDH.
def invertDH (pkIdx: Nat) : Traceful Nat := do
guardTrace brokenDHB
let pk ← receiveMessage pkIdx
let some sk := extractDhSecretKey (X25519.normalizeX25519Key pk) | failure
sendMessage skdef invertKEM
KEM public-key inversion oracle enabled after BrokenKEM.
def invertKEM (pkIdx: Nat) : Traceful Nat := do
guardTrace brokenKEMB
let pk ← receiveMessage pkIdx
let sk ← invertKemPublicKey pk
sendMessage sk
def registerIdentity.
def registerIdentity.reachability: ReachabilityConfig :=
.make (fun p => registerIdentity p)
def registerCorruptIdentity.
def registerCorruptIdentity.reachability: ReachabilityConfig :=
.make (fun ((p, skIdx): Participant × Nat) => registerCorruptIdentity p skIdx)
def genSignedPrekey.
def genSignedPrekey.reachability: ReachabilityConfig :=
.make (fun ((b, idStateIdx): Participant × Nat) => genSignedPrekey b idStateIdx)
def genPQPrekey.
def genPQPrekey.reachability: ReachabilityConfig :=
.make (fun ((b, idStateIdx): Participant × Nat) => genPQPrekey b idStateIdx)
def genOneTimePrekey.
def genOneTimePrekey.reachability: ReachabilityConfig :=
.make (fun b => genOneTimePrekey b)
def compromiseIK.
def compromiseIK.reachability: ReachabilityConfig :=
.make (fun ((p, stateIdx): Participant × Nat) => compromiseIK p stateIdx)
def compromiseSPK.
def compromiseSPK.reachability: ReachabilityConfig :=
.make (fun ((b, stateIdx): Participant × Nat) => compromiseSPK b stateIdx)
def compromisePQSPK.
def compromisePQSPK.reachability: ReachabilityConfig :=
.make (fun ((b, stateIdx): Participant × Nat) => compromisePQSPK b stateIdx)
def compromiseOPK.
def compromiseOPK.reachability: ReachabilityConfig :=
.make (fun ((b, stateIdx): Participant × Nat) => compromiseOPK b stateIdx)
def breakDH.
def breakDH.reachability: ReachabilityConfig :=
.make (fun (_: Unit) => breakDH)
def breakKEM.
def breakKEM.reachability: ReachabilityConfig :=
.make (fun (_: Unit) => breakKEM)
def invertDH.
def invertDH.reachability: ReachabilityConfig :=
.make (fun pkIdx => invertDH pkIdx)
def invertKEM.
def invertKEM.reachability: ReachabilityConfig :=
.make (fun pkIdx => invertKEM pkIdx)endend Reachabilityend DY.Libsignal.PQXDH