1660db8d14
docs: add formal Prolog security proofs
...
Formal verification of NTRU-LWR-OPRF security properties using Scryer Prolog:
- ntru_lwr_oprf.pl: Core proofs (correctness, obliviousness, key recovery)
- noise_analysis.pl: Quantitative noise bounds, LWR correctness conditions
- security_model.pl: Adversarial model, security games, composition theorem
- hash_sensitivity.pl: Why fresh random breaks correctness
Proved properties:
- Correctness: deterministic blinding guarantees same output
- Obliviousness: server cannot learn password (Ring-LWE reduction)
- Key Recovery: requires solving Ring-LWE
- Protocol Unlinkability: AKE wrapper provides session unlinkability
- Composition: Kyber + SymEnc + OPRF maintains all security properties
2026-01-08 12:47:19 -07:00
c034eb5be8
feat(protocol): add AKE wrapper for protocol-level unlinkability
...
Combines NTRU-LWR-OPRF with Kyber key exchange to achieve:
- Correctness: Same password always produces same OPRF output
- Protocol-level unlinkability: Fresh ephemeral keys per session
- Post-quantum security: NTRU Prime (OPRF) + ML-KEM-768 (key exchange)
The OPRF itself is deterministic/linkable, but the encrypted channel
hides OPRF queries from the server, preventing session correlation.
Protocol flow:
1. Client/Server exchange Kyber ephemeral keys
2. Encrypted channel established
3. OPRF query/response sent over encrypted channel
4. Server sees different ciphertexts each session
Tests verify:
- Correctness: same password -> same output across sessions
- Unlinkability: encrypted requests differ between sessions
- Different passwords -> different outputs
2026-01-08 12:09:43 -07:00
8f05b2e157
feat: add mathematical proof tests for OPRF security properties
...
- Add test_proof_of_fingerprint_linkability proving split-blinding is broken
- Add test_proof_of_linkability proving deterministic r,e is linkable
- Add test_proof_of_noise_instability proving fresh random breaks correctness
- Add test_proof_of_fingerprint_in_proposed_fix proving r_pk fix is unlinkable
- Refactor ntru_lwr_oprf.rs for clarity
- Add anyhow dependency for error handling
2026-01-08 12:04:58 -07:00
4e7eec9b91
ntru lwr oprf
2026-01-08 11:01:25 -07:00
12e09718d2
ntru prime
2026-01-08 10:17:25 -07:00
26766bb8d9
changes
2026-01-08 09:50:51 -07:00
50953c7007
docs: add formal security proof for VOLE-LWR OPRF
...
Typst document covering:
- Protocol description and notation
- Ring-LWR and VOLE correlation definitions
- Unlinkability theorem with proof
- Obliviousness theorem with game-based proof
- Output determinism theorem (LWR absorbs noise)
- Security reductions to Ring-LWR and PCG
- Parameter analysis and security estimates
- Comparison with prior art (split-blinding, LEAP)
- Constant-time implementation notes
2026-01-07 14:02:11 -07:00
2d9559838c
feat(oprf): add NTT for O(n log n) multiplication and pure constant-time sampling
...
Performance improvements:
- Replace O(n²) schoolbook multiplication with O(n log n) NTT using Cooley-Tukey/Gentleman-Sande
- ~4x speedup on polynomial multiplication (44ms -> 10ms in tests)
Security improvements:
- Replace branching normalization in sample_small/sample_random_small with ct_normalize
- Add ct_is_negative and ct_normalize constant-time primitives
- All coefficient normalization now uses constant-time operations
NTT implementation:
- Uses q=65537 Fermat prime with primitive 512th root of unity ψ=256
- Precomputed twiddle factors for forward and inverse transforms
- Iterative in-place butterfly with bit-reverse permutation
- Negacyclic convolution for Z_q[X]/(X^n+1)
All 219 tests passing
2026-01-07 13:33:35 -07:00
92b42a60aa
feat(oprf): add constant-time arithmetic and timing attack resistance tests
...
- Fix ct_reduce() to properly handle negative remainders using rem_euclid
- Add comprehensive constant-time primitive tests (ct_reduce, ct_select, ct_eq, ct_lt)
- Add timing attack resistance tests for multiplication, LWR rounding, and eq_approx
- Verify timing ratios are independent of coefficient values
- All 219 tests passing with 0 warnings
2026-01-07 13:14:42 -07:00
9c4a3a30b6
feat(oprf): add production-grade Silent VOLE authentication protocol
...
Implements complete registration + login flow:
- Registration: Client/Server exchange PCG seeds (once)
- Login: Single-round (pcg_index + masked_input → evaluation)
New types:
- VoleRegistrationRequest/Response - PCG seed exchange
- VoleUserRecord - Server's stored user data
- VoleClientCredential - Client's stored credential
- VoleLoginRequest/Response - Single-round login messages
Key properties:
- Single-round online phase after registration
- Perfect privacy (server cannot fingerprint users)
- ~4KB round-trip (vs ~8KB for Ring-LPR)
- Deterministic OPRF output (LWR guaranteed)
- Wrong password correctly rejected
All 211 tests passing.
2026-01-07 13:04:14 -07:00
d8b4ed9c2d
feat(oprf): add revolutionary VOLE-LWR helper-less unlinkable OPRF
...
Implements a novel post-quantum OPRF combining:
- VOLE-based masking (prevents fingerprint attacks)
- LWR finalization (no reconciliation helpers transmitted)
- PCG pre-processing (amortized communication cost)
- NTT-friendly q=65537 (WASM performance)
Key fixes during implementation:
- LWR parameters: p=16, β=1 ensures 2nβ²=512 < q/(2p)=2048
- Password element must be UNIFORM (not small) for LWR to work
- Server subtracts v=u·Δ+noise, client just rounds (no addition)
Performance: ~82µs full protocol (vs 60µs fast, 99µs unlinkable)
Security: UC-unlinkable, helper-less, post-quantum (Ring-LWR)
All 206 tests passing.
2026-01-07 12:59:20 -07:00
8d58a39c3b
feat(oprf): add LEAP-style truly unlinkable OPRF with commit-challenge protocol
...
- Implement commit-challenge protocol to prevent fingerprint attack
- Use Learning With Rounding (LWR) instead of reconciliation helpers
- Add mathematical analysis document (docs/LEAP_ANALYSIS.md)
- 8 new tests, 197 total tests passing
- Benchmark: ~108µs (102x faster than OT-based, truly unlinkable)
The key insight: client commits to r BEFORE server sends challenge ρ,
so server cannot predict H(r||ρ) to extract A·s+e fingerprint.
2026-01-07 12:36:44 -07:00
f022aeefd6
feat(oprf): add split-blinding unlinkable OPRF (partial unlinkability)
...
- Implement split-blinding protocol with C, C_r dual evaluation
- Add 7 security proof tests for unlinkability properties
- Add benchmarks: ~101µs (109x faster than OT-based)
- Note: Server can compute C - C_r fingerprint (documented limitation)
2026-01-07 12:29:15 -07:00
9be4bcaf7d
initial
2026-01-07 11:40:09 -07:00
44e60097e3
Add forward secrecy, server impersonation, MITM resistance, and quantum security tests
2026-01-06 16:10:24 -07:00
acc8dde789
Fixed reconciliation bug - Peikert-style reconciliation now achieves 100% accuracy (was 50% with broken XOR)
2026-01-06 15:57:16 -07:00
e893d6998f
Fixed reconciliation bug - Peikert-style reconciliation now achieves 100% accuracy (was 50% with broken XOR)
2026-01-06 13:23:40 -07:00
053b983f43
feat: used Peikert-style reconciliation rather than XOR which led to 50% reconcilation
2026-01-06 13:11:20 -07:00
0099a6e1fb
proofs
2026-01-06 12:55:40 -07:00
dfa968ec7d
initial
2026-01-06 12:49:26 -07:00
