Quantum Cryptography and Autoformalization in Lean

Maor Ben Shahar, Jonathan Morag, Dirk Englund, Kfir Sulimany

arXivarxiv/2610.17286Oct 12, 2026quant-phscore 0

Quantum key distribution provides secure communication by relying on physics principles and mathematical reasoning. Security proofs across the field can contain gaps, often between individually valid theorems integrated under mismatched assumptions. We produce an end-to-end security theorem formalized in the Lean proof assistant, eliminating hidden hypotheses by building only on Lean's standard axioms. Our proof covers composable security of the entanglement-based qubit BB84 protocol against coherent attacks by the postselection technique, accounting for finite block size, and is written in…

SourceJSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/arxiv/2610.17286
curl -X POST /api/v1/records/arxiv/2610.17286/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2610.17286/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'