diff --git a/PQXDHLean/AEAD.lean b/PQXDHLean/AEAD.lean
index 30e2205..1fcc9df 100644
--- a/PQXDHLean/AEAD.lean
+++ b/PQXDHLean/AEAD.lean
@@ -1,7 +1,31 @@
 /-
 Authenticated Encryption with Associated Data (AEAD).
 
-Definitions follow Bhargavan et al., USENIX Security 2024.
+Definitions follow Bhargavan et al., USENIX Security 2024, §2.1.
+Signal uses AES-256-CBC + HMAC in Encrypt-then-MAC mode.
+
+## Current scope
+
+This structure suffices for **correctness proofs** (X3DH_handshake_correct):
+  - `encrypt` and `decrypt` are deterministic
+  - Nonce is omitted — X3DH uses each session key exactly once
+
+## Future work (security proofs)
+
+When filling in the IND-CPA + INT-CTXT security proof (Theorem 2,
+§3.2), two extensions may be needed:
+
+  1. **Nonce parameter**: Real AEAD requires a nonce to avoid
+     key-nonce reuse. The paper shows `enc(msg, 0, AD, SK)` where
+     `0` is the nonce. For a general AEAD formalization, `encrypt`
+     should become `K → PT → Nonce → AD → CT`.
+
+  2. **Probabilistic encryption**: Some AEAD modes involve
+     randomness (e.g., IV generation). Security proofs (IND-CPA)
+     may require `encrypt` to be an `OracleComp unifSpec`.
+
+The security assumption (IND-CPA + INT-CTXT) is formalized
+separately in `SecurityDefs.lean` as an `opaque Prop`.
 -/
 
 /-- AEAD scheme parameterized by key `K`, plaintext `PT`, ciphertext `CT`,
diff --git a/PQXDHLean/KEM.lean b/PQXDHLean/KEM.lean
index 7c23fc5..6186546 100644
--- a/PQXDHLean/KEM.lean
+++ b/PQXDHLean/KEM.lean
@@ -1,7 +1,30 @@
 /-
 Key Encapsulation Mechanism (KEM).
 
-Definitions follow Bhargavan et al., USENIX Security 2024.
+Definitions follow Bhargavan et al., USENIX Security 2024, §2.1.
+
+## Current scope
+
+This structure suffices for **correctness proofs** (PQXDH_agree):
+  - `encaps` and `decaps` are deterministic
+  - `keygen` is omitted — callers supply matching (pk, sk) pairs
+
+## Future work (security proofs)
+
+When filling in the IND-CCA security proof (Theorem 3, §3.2) or
+the SH-CR proof (Theorem 5, §4), two extensions are needed:
+
+  1. **`keygen`**: The IND-CCA game begins with `(pk, sk) ← KEM.keygen`.
+     This should be a probabilistic operation (`OracleComp unifSpec`).
+
+  2. **Probabilistic `encaps`**: Real KEM encapsulation is randomized.
+     For security proofs, `encaps` should become
+     `PK → OracleComp unifSpec (CT × SS)`, similar to how `KDF` has
+     a deterministic form (`KDF.derive`) and a probabilistic form
+     (`KDFOracle` as a random oracle).
+
+  One approach: introduce a separate `KEMSpec` (probabilistic, for
+  security) alongside this `KEM` (deterministic, for correctness).
 -/
 
 /-- KEM parameterized by public key `PK`, secret key `SK_kem`,
diff --git a/PQXDHLean/X3DH/X3DH.lean b/PQXDHLean/X3DH/X3DH.lean
index 738063b..4b815e9 100644
--- a/PQXDHLean/X3DH/X3DH.lean
+++ b/PQXDHLean/X3DH/X3DH.lean
@@ -38,6 +38,11 @@ structure KeyPair (F G : Type _) [Field F] [AddCommGroup G] [Module F G]
 
 /-! ## X3DH shared secret computation
 
+**Notation convention:**
+  - Lowercase names (`ikₐ`, `ekₐ`, `spkᵦ`, `opkᵦ`) denote **private keys** (scalars in `F`)
+  - Uppercase names (`IKᵦ`, `SPKᵦ`, `OPKᵦ`) denote **public keys** (group elements in `G`)
+  - Subscripts `ₐ` / `ᵦ` indicate the owner (Alice / Bob)
+
 Alice and Bob each compute DH values from their private keys
 and the other party's public keys:
 
@@ -98,13 +103,13 @@ def X3DH_SK_Alice
     (ikₐ ekₐ : F) (IKᵦ SPKᵦ : G) (OPKᵦ : Option G) : SK :=
   kdf.derive (X3DH_Alice ikₐ ekₐ IKᵦ SPKᵦ OPKᵦ)
 
-/-- Bob derives the session key SK_B = KDF(DH1 ‖ DH2 ‖ DH3 ‖ DH4). -/
+/-- Bob derives the session key SKᵦ = KDF(DH1 ‖ DH2 ‖ DH3 ‖ DH4). -/
 def X3DH_SK_Bob
     (kdf : KDF (G × G × G × G) SK)
     (ikᵦ spkᵦ : F) (opkᵦ : Option F) (IKₐ EKₐ : G) : SK :=
   kdf.derive (X3DH_Bob ikᵦ spkᵦ opkᵦ IKₐ EKₐ)
 
-/-- Session key agreement: SKₐ = SK_B.
+/-- Session key agreement: SKₐ = SKᵦ.
 Composes `X3DH_agree` with the determinism of the KDF. -/
 theorem X3DH_session_key_agree
     (kdf : KDF (G × G × G × G) SK)
diff --git a/PQXDHLean/X3DH/X3DHPassiveMessageSecrecy.lean b/PQXDHLean/X3DH/X3DHPassiveMessageSecrecy.lean
index e8a70af..a3b27cc 100644
--- a/PQXDHLean/X3DH/X3DHPassiveMessageSecrecy.lean
+++ b/PQXDHLean/X3DH/X3DHPassiveMessageSecrecy.lean
@@ -9,11 +9,14 @@ distinguish the session key from a random key.
 
 ## The game
 
-  1. Sample all private keys uniformly from F.
+  1. Sample the 5 private keys uniformly from F:
+     ikₐ, ekₐ (Alice's identity + ephemeral),
+     ikᵦ, spkᵦ, opkᵦ (Bob's identity + signed prekey + one-time prekey).
   2. Compute public keys and the four DH values via X3DH.
   3. Query the KDF oracle (random oracle) on the DH tuple to get
      the real session key.
-  4. Sample a random key.
+  4. Sample a random key uniformly from SK (same distribution as the
+     KDF's output space).
   5. Flip a bit b; give the adversary the public transcript
      and either the real key (b = true) or the random key.
   6. The adversary outputs a guess b'.
@@ -170,6 +173,13 @@ The reduction receives the DDH challenge `(g, EKₐ, SPKᵦ, T)`,
 embeds T as DH3, queries the ROM on the resulting DH tuple to
 get a session key, and passes it directly to the adversary.
 
+Why DH3? Among the four X3DH DH values, DH3 = ekₐ • SPKᵦ is the
+only one whose computation needs both of the secret scalars
+hidden in the DDH challenge (ekₐ and spkᵦ). The other DH values
+(DH1, DH2, DH4) each involve at least one scalar the reduction
+samples itself (ikₐ, ikᵦ, or opkᵦ), so they can be computed
+honestly. Embedding T at DH3 is what makes the reduction possible.
+
 No internal coin flip — the DDH experiment's own bit handles
 the real/random branching. The reduction simply forwards the
 adversary's guess. -/