|
|
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 |
|
