Files
opaque-lattice/SECURITY_PROOF.md
2026-01-06 12:49:26 -07:00

591 lines
18 KiB
Markdown
Raw Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
# UC Security Proof for Lattice-Based OPAQUE
This document provides a formal security proof for the opaque-lattice implementation in the Universal Composability (UC) framework.
## Table of Contents
1. [Overview](#1-overview)
2. [Preliminaries](#2-preliminaries)
3. [Ideal Functionalities](#3-ideal-functionalities)
4. [Protocol Description](#4-protocol-description)
5. [Simulator Construction](#5-simulator-construction)
6. [Security Proof](#6-security-proof)
7. [Concrete Security Bounds](#7-concrete-security-bounds)
---
## 1. Overview
### 1.1 Protocol Summary
opaque-lattice implements a post-quantum secure OPAQUE protocol using:
- **Ring-LPR OPRF**: Oblivious PRF based on Ring Learning Parity with Rounding
- **ML-KEM (Kyber768)**: Key encapsulation for authenticated key exchange
- **ML-DSA (Dilithium3)**: Digital signatures for server authentication
- **VOPRF Extension**: Verifiable OPRF with Lyubashevsky-style sigma protocol
### 1.2 Security Goals
We prove the protocol realizes the ideal functionality F_aPAKE (asymmetric Password-Authenticated Key Exchange) with the following properties:
| Property | Description |
|----------|-------------|
| **Password Obliviousness** | Server learns nothing about password during OPRF |
| **Forward Secrecy** | Compromise of long-term keys doesn't reveal past session keys |
| **Server Compromise Resistance** | Attacker cannot offline-attack passwords after server compromise |
| **Quantum Resistance** | Security holds against quantum adversaries |
| **Verifiability** | Client can verify server used consistent OPRF key |
### 1.3 Security Model
We work in the UC framework of Canetti [Can01] with:
- **Global Random Oracle Model (GROM)**: Hash functions H₁, H₂, H₃ modeled as random oracles
- **Adaptive Corruptions**: Adversary can corrupt parties at any point
- **Static Compromise**: Adversary learns all internal state upon corruption
---
## 2. Preliminaries
### 2.1 Notation
| Symbol | Meaning |
|--------|---------|
| λ | Security parameter (128 bits) |
| R | Ring Z[x]/(x^n + 1) where n = 256 |
| R_q | Ring R modulo q (q = 4 in our construction) |
| ⌊·⌋₁ | Deterministic rounding: ⌊x⌋₁ = ⌊x/2⌋ mod 2 |
| k ←$ S | Sample k uniformly from set S |
| negl(λ) | Negligible function in λ |
| poly(λ) | Polynomial function in λ |
### 2.2 Computational Assumptions
**Definition 2.1 (Ring-LPR Problem)**
For a ∈ R₂, s ∈ R₂, the Ring Learning Parity with Rounding problem states that:
```
(a, ⌊a·s mod 4⌋₁) ≈_c (a, ⌊u⌋₁)
```
where u ←$ R₄ is uniform random.
**Definition 2.2 (Dihedral Coset Problem)**
Given quantum states encoding cosets of a hidden subgroup in the dihedral group D_n, find the hidden subgroup generator. Time complexity: O(e^n) even for quantum computers.
**Theorem 2.1 (Security Reduction Chain)**
```
Ring-LPR → LPR → LWR → G-EDCP → DCP
```
Each reduction is polynomial-time. The DCP problem is believed quantum-hard with time complexity O(e^n).
**Definition 2.3 (ML-KEM Security)**
ML-KEM (Kyber768) is IND-CCA2 secure under the Module-LWE assumption.
**Definition 2.4 (ML-DSA Security)**
ML-DSA (Dilithium3) is EUF-CMA secure under the Module-LWE and Module-SIS assumptions.
### 2.3 Building Blocks
**PRF Construction (Ring-LPR)**
```
F_k(x) = H₂(⌊k · H₁(x) mod 4⌋₁)
```
where:
- H₁: {0,1}* → R₂ (hash-to-ring)
- H₂: R₁ → {0,1}^512 (ring-to-output hash)
- k ∈ R₂ (secret key)
**Key Commitment**
```
Commit(k; r) = H₃(k || r)
```
where r ←$ {0,1}^256 is randomness.
---
## 3. Ideal Functionalities
### 3.1 Ideal VOPRF Functionality F_VOPRF
```
Functionality F_VOPRF
Parameters: Output length l, security parameter λ
Initialization:
- On (Init, sid) from server S:
- If first Init for sid: set T_sid(·) = ⊥, tx(S) = 0
- Send (Init, sid, S) to adversary A
- On (Param, S, π) from A:
- If params[S] undefined: set params[S] = π
Key Commitment:
- On (Commit, sid) from S:
- Sample random table key k_sid
- Store commitment c = H(k_sid)
- Send (Committed, sid, c) to A
Offline Evaluation:
- On (OfflineEval, sid, c, p) from party P:
- If params[i] = c for some server i:
- If T_sid(i, p) undefined: T_sid(i, p) ←$ {0,1}^l
- Send (OfflineEval, sid, T_sid(i, p)) to P
- Else: ignore
Online Evaluation:
- On (Eval, sid, ssid, S, p) from user U:
- Record ⟨ssid, S, U, p⟩
- Send (Eval, sid, ssid, U, S) to A
- On (SndrComplete, sid, ssid) from S:
- Increment tx(S)
- Send (SndrComplete, sid, ssid, S) to A
- On (RcvCmplt, sid, ssid, U, π) from A:
- Retrieve ⟨ssid, S, U, p⟩
- Ignore if:
- No such record exists
- Honest server S has params[S] = π but tx(S) = 0
- S honest but π ≠ params[S]
- If T_sid(i, p) undefined: T_sid(i, p) ←$ {0,1}^l
- Send (Eval, sid, ssid, T_sid(i, p)) to U
- Decrement tx(S) if params[S] = π
Verification:
- On (Verify, sid, c, p, y, proof) from U:
- Check if y = T_sid(i, p) for params[i] = c
- Send (Verified, sid, valid/invalid) to U
```
### 3.2 Ideal AKE Functionality F_AKE
```
Functionality F_AKE
Initialization:
- Maintain session table sessions[·]
- Maintain corruption set Corrupt
Key Exchange:
- On (NewSession, sid, P, P', role) from party P:
- Record (sid, P, P', role, ⊥)
- Send (NewSession, sid, P, P', role) to A
- On (TestPwd, sid, P, pw') from A:
- If P ∈ Corrupt: return ⊥
- Retrieve (sid, P, P', role, pw)
- If pw' = pw: mark session compromised
- Return (compromised/not-compromised)
- On (NewKey, sid, P, sk) from A:
- Retrieve (sid, P, P', role, pw)
- If P' ∈ Corrupt or session compromised:
- Output (sid, sk) to P
- Else if (sid, P', P, role', k') exists with k' ≠ ⊥:
- Output (sid, k') to P
- Else:
- Sample k ←$ {0,1}^λ
- Record k, output (sid, k) to P
```
### 3.3 Ideal aPAKE Functionality F_aPAKE
```
Functionality F_aPAKE
Parameters: Security parameter λ
Registration:
- On (Register, sid, U, S, pw) from user U:
- Compute file ← F_OPRF.Eval(pw)
- Store (U, file) for server S
- Send (Registered, sid, U) to S
Login:
- On (Login, sid, U, S, pw) from U:
- Initiate OPRF evaluation with S
- If pw matches stored file:
- Derive session key sk
- Output (LoginComplete, sid, sk) to U, S
- Else:
- Output (LoginFailed, sid) to U
Server Compromise:
- On (Corrupt, S) from A:
- Add S to Corrupt set
- Send all stored files to A
- Note: Offline attacks still require online OPRF interaction
```
---
## 4. Protocol Description
### 4.1 Registration Protocol
```
Client(pw) Server(oprf_key)
═══════════════════════════════════════════════════════════════
1. salt ←$ {0,1}^256
2. pw_hash = Argon2id(pw, salt)
3. (state, blind) = OPRF.Blind(pw_hash)
─────── blind ───────────►
4. eval = OPRF.Eval(oprf_key, blind)
◄────── eval ─────────
5. rw = OPRF.Finalize(state, eval)
6. (pk_U, sk_U) = KEM.KeyGen()
7. (pk_auth, sk_auth) = SIG.KeyGen()
8. envelope = AEAD.Enc(rw, sk_U || sk_auth)
9. record = (pk_U, pk_auth, envelope, salt)
─────── record ──────────►
10. Store(U, record)
```
### 4.2 Login Protocol (KE1 → KE2 → KE3)
```
Client(pw) Server(oprf_key, record)
═══════════════════════════════════════════════════════════════
KE1: Client → Server
1. pw_hash = Argon2id(pw, record.salt)
2. (state, blind) = OPRF.Blind(pw_hash)
3. (ek_C, dk_C) = KEM.KeyGen()
───── KE1: (blind, ek_C) ─────►
KE2: Server → Client
4. eval = OPRF.Eval(oprf_key, blind)
5. (ct, ss_S) = KEM.Encap(ek_C)
6. K_session = KDF(ss_S, transcript)
7. mac_S = MAC(K_session, transcript)
8. sig = SIG.Sign(sk_S, transcript)
◄─── KE2: (eval, ct, mac_S, sig, envelope) ───
KE3: Client → Server
9. Verify sig with pk_S
10. rw = OPRF.Finalize(state, eval)
11. (sk_U, sk_auth) = AEAD.Dec(rw, envelope)
12. ss_C = KEM.Decap(dk_C, ct)
13. K_session = KDF(ss_C, transcript)
14. Verify mac_S
15. mac_C = MAC(K_session, transcript)
───── KE3: mac_C ─────►
16. Verify mac_C
17. Output K_session Output K_session
```
### 4.3 VOPRF Extension
For verifiable evaluation, server additionally:
```
Server with committed key (k, c, r):
1. Compute eval = F_k(blind)
2. Generate ZK proof π proving:
- Knowledge of k such that c = Commit(k; r)
- eval = F_k(blind)
3. Return (eval, π)
Client:
1. Verify π against commitment c
2. If valid: proceed with finalization
3. If invalid: abort
```
---
## 5. Simulator Construction
### 5.1 Simulator for F_VOPRF
```
Simulator SIM_VOPRF
On (Init, sid, S) from F_VOPRF:
- Sample random key k_sim
- Compute c = Commit(k_sim; r_sim)
- Send (Param, S, c) to F_VOPRF
- Record (S, k_sim, r_sim, c)
On (Eval, sid, ssid, U, S) from F_VOPRF:
If S honest:
- Wait for adversary to deliver
- On delivery: send (SndrComplete, sid, ssid) to F_VOPRF
- Send (RcvCmplt, sid, ssid, U, c_S) to F_VOPRF
If S corrupted:
- Extract adversary's evaluation blind_A
- Query F_VOPRF for T_sid(c_A, blind_A)
- Program H₂ to output T_sid value
- Simulate protocol messages
On H₂ query (x, y, c) from A:
If ∃ honest S with params[S] = c:
- Send (OfflineEval, sid, c, H₁⁻¹(x)) to F_VOPRF
- Receive ρ from F_VOPRF
- Return ρ
Else:
- Return random value or use table
```
### 5.2 Simulator for F_aPAKE
```
Simulator SIM_aPAKE
Registration Simulation:
On (Register, sid, U, S, pw) from F_aPAKE:
- Simulate OPRF blind message
- Receive adversarial evaluation
- Extract any password guesses
- Complete registration
Login Simulation (Honest Client, Honest Server):
- Simulate KE1 with random blind
- Simulate KE2 with random evaluation
- On (TestPwd, sid, U, pw') from A:
- Forward to F_aPAKE
- If compromised: program keys accordingly
- Generate session key from F_aPAKE
- Program MAC/KDF oracles consistently
Login Simulation (Corrupted Server):
- Extract server's OPRF key from state
- Use real OPRF evaluation
- Monitor password test queries
- Enforce "one online guess per session"
Login Simulation (Corrupted Client):
- Extract client's password from state
- Use real protocol execution
- Provide adversary with session key
```
---
## 6. Security Proof
### 6.1 Main Theorem
**Theorem 6.1 (UC Security)**
The opaque-lattice protocol UC-realizes F_aPAKE in the (F_VOPRF, F_RO)-hybrid model, assuming:
1. Ring-LPR is pseudorandom (Definition 2.1)
2. ML-KEM is IND-CCA2 secure
3. ML-DSA is EUF-CMA secure
4. AEAD is IND-CPA and INT-CTXT secure
5. HKDF is a secure PRF
The advantage of any PPT adversary A in distinguishing real from ideal execution is:
```
Adv(A) ≤ q_pwd · Adv_LPR + q_KEM · Adv_IND-CCA + q_SIG · Adv_EUF-CMA
+ q_AEAD · Adv_AEAD + q_sessions · negl(λ)
```
where q_* denotes the number of respective queries.
### 6.2 Proof by Game Sequence
**Game 0 (Real Protocol)**
The real execution of opaque-lattice with adversary A.
**Game 1 (Random Oracle Instrumentation)**
Replace hash functions H₁, H₂, H₃ with random oracles maintained by simulator.
- Indistinguishable by random oracle assumption
**Game 2 (OPRF Simulation)**
Replace real OPRF evaluations with queries to F_VOPRF.
- For honest server: outputs are random (Ring-LPR pseudorandomness)
- For corrupted server: extract key, compute real evaluation
*Lemma 6.1:* |Pr[Game 2] - Pr[Game 1]| ≤ q_oprf · Adv_LPR
**Game 3 (KEM Simulation)**
Replace KEM encapsulation with F_KEM ideal functionality.
- Honest parties: shared secret is random
- Corrupted parties: extract/inject values
*Lemma 6.2:* |Pr[Game 3] - Pr[Game 2]| ≤ q_kem · Adv_IND-CCA
**Game 4 (Signature Simulation)**
Replace signatures with F_SIG ideal functionality.
- Verify signatures using committed public key
- Reject any forgeries
*Lemma 6.3:* |Pr[Game 4] - Pr[Game 3]| ≤ q_sig · Adv_EUF-CMA
**Game 5 (Envelope Simulation)**
Replace AEAD with ideal encryption.
- Envelope contents are hidden until rw is known
- Tampering detected by INT-CTXT
*Lemma 6.4:* |Pr[Game 5] - Pr[Game 4]| ≤ q_aead · Adv_AEAD
**Game 6 (Password Test Restriction)**
Enforce that adversary must make explicit TestPwd query to F_aPAKE.
- Each online session allows at most one password test
- Offline dictionary attack requires OPRF evaluation
*Lemma 6.5:* |Pr[Game 6] - Pr[Game 5]| ≤ negl(λ)
**Game 7 (Ideal Execution)**
Execute with F_aPAKE and simulator SIM.
- Session keys are random unless compromised
- Password never revealed to honest parties
*Lemma 6.6:* Game 6 ≡ Game 7
### 6.3 Verifiability Proof
**Theorem 6.2 (VOPRF Soundness)**
For any PPT adversary A, the probability that A produces a valid proof π for an evaluation y = F_k(x) where k differs from the committed key is negligible.
*Proof Sketch:*
1. By binding property of commitment: A cannot open to different k
2. By soundness of sigma protocol: A cannot forge proofs
3. By Fiat-Shamir security: Non-interactive proofs are sound in ROM
**Theorem 6.3 (VOPRF Zero-Knowledge)**
The sigma protocol proof reveals nothing about k beyond the validity of the statement.
*Proof Sketch:*
1. Construct simulator S that generates accepting proofs without k
2. S samples response z uniformly, computes mask m = z - e·k_dummy
3. By rejection sampling analysis: real and simulated distributions are statistically close
4. Distinguishing advantage bounded by 2^(-λ)
---
## 7. Concrete Security Bounds
### 7.1 Parameter Selection
| Parameter | Value | Security Level |
|-----------|-------|----------------|
| Ring dimension n | 256 | 128-bit post-quantum |
| Ring modulus q | 4 | Minimal for rounding |
| KEM security | Kyber768 | NIST Level 3 |
| Signature security | Dilithium3 | NIST Level 3 |
| Hash output | 512 bits | Collision resistance |
| Commitment nonce | 256 bits | Binding security |
### 7.2 Concrete Advantages
Assuming λ = 128 security parameter:
| Component | Advantage Bound |
|-----------|-----------------|
| Ring-LPR PRF | 2^(-128) (DCP hardness) |
| ML-KEM IND-CCA | 2^(-128) (MLWE hardness) |
| ML-DSA EUF-CMA | 2^(-128) (MLWE+SIS hardness) |
| AEAD (AES-GCM) | 2^(-128) |
| HKDF-SHA512 | 2^(-256) |
| Commitment binding | 2^(-128) (collision resistance) |
| ZK soundness | 2^(-128) (sigma protocol) |
### 7.3 Attack Complexity
| Attack | Complexity | Mitigation |
|--------|------------|------------|
| Offline dictionary | Requires OPRF oracle | One guess per session |
| Online brute force | O(2^128) sessions | Rate limiting |
| Quantum OPRF attack | O(e^256) | DCP hardness |
| Server compromise | No offline attack | OPRF obliviousness |
| Forward secrecy break | O(2^128) per session | Ephemeral KEM keys |
---
## References
[Can01] R. Canetti. "Universally Composable Security: A New Paradigm for Cryptographic Protocols." FOCS 2001.
[JKX18] S. Jarecki, H. Krawczyk, J. Xu. "OPAQUE: An Asymmetric PAKE Protocol Secure Against Pre-Computation Attacks." Eurocrypt 2018.
[Lyu09] V. Lyubashevsky. "Fiat-Shamir with Aborts: Applications to Lattice and Factoring-Based Signatures." ASIACRYPT 2009.
[Lyu12] V. Lyubashevsky. "Lattice Signatures without Trapdoors." EUROCRYPT 2012.
[Sha25] Z. Shan et al. "Fast Post-Quantum Private Set Intersection from Ring-LPR OPRF." J. Syst. Arch. 2025.
[Alb21] M. Albrecht et al. "Round-optimal Verifiable OPRFs from Ideal Lattices." PKC 2021.
[Fal22] J. Faller. "Composable OPRFs via Garbled Circuits." Master's Thesis, 2022.
[RFC9807] RFC 9807. "The OPAQUE Augmented PAKE Protocol." 2024.
---
## Appendix A: Proof Details
### A.1 Ring-LPR Pseudorandomness
**Lemma A.1** For uniformly random k ∈ R₂ and arbitrary x ∈ R₂:
```
{(x, F_k(x))} ≈_c {(x, U)}
```
where U is uniform random output.
*Proof:*
1. F_k(x) = H₂(⌊k·x mod 4⌋₁)
2. By Ring-LPR assumption: ⌊k·x mod 4⌋₁ ≈_c ⌊u⌋₁ for random u
3. H₂ is a random oracle: output is uniformly distributed
4. Combining: F_k(x) is computationally indistinguishable from random
### A.2 Sigma Protocol Analysis
**Commitment:**
```
t = H(m || m·a)
```
where m ←$ R_q with small coefficients.
**Challenge:**
```
e = H(c || t || x || y)[0:16]
```
(128-bit challenge via Fiat-Shamir)
**Response:**
```
z = m + e·k
```
with rejection if ||z||_∞ > B.
**Rejection Probability:**
By Lemma 4.1 of [Lyu12], if m is sampled from discrete Gaussian with σ > 12·||k||:
```
Pr[rejection] ≤ 2^(-100)
```
**Soundness:**
If adversary produces accepting proofs for (c, x, y₁) and (c, x, y₂) with y₁ ≠ y₂:
```
z₁ - z₂ = e₁·k - e₂·k = (e₁ - e₂)·k
```
Since e₁ ≠ e₂ with overwhelming probability, we can extract k.
**Zero-Knowledge:**
Simulator chooses z uniformly, computes t = H(z - e·k_dummy || ...), programs RO.
Statistical distance from real: 2^(-λ) by rejection sampling lemma.
---
## Appendix B: Implementation Notes
### B.1 Constant-Time Implementation
All operations on secret data must be constant-time:
- Ring multiplication: coefficient-by-coefficient, no early termination
- Rounding: table lookup with constant access pattern
- Comparison: bitwise operations only
### B.2 Side-Channel Mitigations
- **Timing attacks**: All branches on secret data eliminated
- **Cache attacks**: No secret-dependent memory access patterns
- **Power analysis**: Balanced operations where possible
### B.3 Zeroization
All secret values are zeroized after use:
- OPRF keys: `RingLprKey` implements `ZeroizeOnDrop`
- Session keys: explicit zeroize before deallocation
- Intermediate values: scoped to minimize lifetime