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

.cargo

changes

2026-01-08 09:50:51 -07:00

benches

feat(oprf): add revolutionary VOLE-LWR helper-less unlinkable OPRF

2026-01-07 12:59:20 -07:00

docs

docs: add formal security proof for VOLE-LWR OPRF

2026-01-07 14:02:11 -07:00

papers

initial

2026-01-06 12:49:26 -07:00

papers_txt

initial

2026-01-06 12:49:26 -07:00

pdfs

changes

2026-01-08 09:50:51 -07:00

proofs

docs: add formal Prolog security proofs

2026-01-08 12:47:19 -07:00

src

feat(protocol): add AKE wrapper for protocol-level unlinkability

2026-01-08 12:09:43 -07:00

.gitignore

initial

2026-01-06 12:49:26 -07:00

Cargo.toml

feat: add mathematical proof tests for OPRF security properties

2026-01-08 12:04:58 -07:00

idk2.txt

Fixed reconciliation bug - Peikert-style reconciliation now achieves 100% accuracy (was 50% with broken XOR)

2026-01-06 15:57:16 -07:00

PLAN.md

initial

2026-01-06 12:49:26 -07:00

SECURITY_PROOF.md

initial

2026-01-07 11:40:09 -07:00

Description

No description provided

113 MiB

Languages

Rust 52.6%

HTML 47.4%