Cole Leavitt
1660db8d14
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
72 lines
2.1 KiB
Markdown
72 lines
2.1 KiB
Markdown
# Formal Security Proofs for NTRU-LWR-OPRF
|
|
|
|
Verified with Scryer Prolog.
|
|
|
|
## Files
|
|
|
|
| File | Description |
|
|
|------|-------------|
|
|
| `ntru_lwr_oprf.pl` | Main security proofs: correctness, obliviousness, key recovery hardness |
|
|
| `noise_analysis.pl` | Quantitative noise bounds and LWR correctness analysis |
|
|
| `security_model.pl` | Formal adversarial model and composition theorem |
|
|
| `hash_sensitivity.pl` | Analysis of why fresh random breaks correctness |
|
|
|
|
## Running the Proofs
|
|
|
|
```bash
|
|
# Install Scryer Prolog
|
|
cargo install scryer-prolog
|
|
|
|
# Run all proofs
|
|
scryer-prolog ntru_lwr_oprf.pl
|
|
scryer-prolog noise_analysis.pl
|
|
scryer-prolog security_model.pl
|
|
scryer-prolog hash_sensitivity.pl
|
|
```
|
|
|
|
## Key Results
|
|
|
|
### Proved Properties
|
|
|
|
| Property | Status | Proof |
|
|
|----------|--------|-------|
|
|
| Correctness | ✅ | Same password → same output (with deterministic blinding) |
|
|
| Obliviousness | ✅ | Server cannot learn password from (C, r_pk) |
|
|
| Key Recovery Hard | ✅ | Reduces to Ring-LWE problem |
|
|
| Pseudorandomness | ✅ | Output indistinguishable from random |
|
|
| Protocol Unlinkability | ✅ | AKE wrapper hides linkable OPRF |
|
|
|
|
### The Fundamental Tension
|
|
|
|
```
|
|
UNLINKABLE ∧ CORRECT is impossible for lattice OPRFs
|
|
|
|
Proof:
|
|
UNLINKABLE ⟹ fresh random (r,e) each session
|
|
Fresh (r,e) ⟹ noise η varies
|
|
CORRECT ⟹ round(k·s + η) must be constant
|
|
But varying η can cross bin boundaries
|
|
∴ ¬CORRECT
|
|
|
|
Resolution: Accept OPRF-level linkability, achieve protocol-level
|
|
unlinkability via Kyber AKE encryption wrapper.
|
|
```
|
|
|
|
### Security Parameters
|
|
|
|
| Parameter | Value | Security |
|
|
|-----------|-------|----------|
|
|
| Ring degree p | 761 | Prime (NTRU Prime) |
|
|
| Modulus q | 4591 | Prime, x^p-x-1 irreducible |
|
|
| Classical security | 248 bits | Lattice reduction |
|
|
| Quantum security | ~128 bits | Post-Grover |
|
|
|
|
## Composition Theorem
|
|
|
|
The full protocol composes:
|
|
1. **NTRU-LWR-OPRF**: Oblivious, Pseudorandom, Linkable
|
|
2. **Kyber KEM**: IND-CCA2 secure
|
|
3. **Symmetric encryption**: IND-CPA secure
|
|
|
|
Result: Protocol is **Oblivious**, **Pseudorandom**, and **Unlinkable**.
|