FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq

Quantum key distribution QKD, whose security is derived from quantum mechanics rather than computational assumptions, is moving into standardization and commercial deployment. Yet its security guarantees rest on technically delicate proofs checked by hand. Formal verification closes this gap,...

Quantum Cryptography and Autoformalization in Lean

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

QIAP: A Quantum-Inspired Authentication Protocol with BB84-Based Channel Monitoring

Authentication in quantum-aware communication settings requires mechanisms that verify user legitimacy while also assessing whether the communication channel exhibits excessive disturbance. This paper presents QIAP, a stateful hybrid framework that combines classical commitment-based...

Performance Analysis of Multiparty GHZ-State Quantum Conference Key Agreement over Optical Fiber Channel

Quantum conference key agreement QCKA enables multiple spatially separated users to establish a common key with composable information-theoretic security by exploiting multipartite quantum correlations. Greenberger--Horne--Zeilinger GHZ states are a natural resource for this task, but their...

Constant-Rate Certified Deletion

We present a unified framework for upgrading a broad class of cryptographic primitives to support constant-rate certified deletion. Previous constructions require a linear number of qubits per encrypted bit of certified-deletable plaintext. In contrast, we obtain the first constant-rate...

Breaking the Bounded Entanglement Barrier for Quantum Position Verification

Position verification, introduced by Chandran et al. SIAM J. Computing 2014, allows verifiers to test a prover's claimed position by an interactive protocol. Classical position verification is impossible. Even for Quantum Position Verification QPV, there always exists an LOCC Local Operations and...

Semi-Quantum Cryptography with Certified Deletion

Certified deletion allows a client to upload encrypted data to a server as a quantum state, then later request that the server delete their data and detect whether the server complies. If verification passes, then the data on the server will remain hidden even if the decryption key is later leake...

Security Framework for Practical Quantum Key Distribution with Imperfect Devices

Practical quantum key distribution QKD systems inevitably exhibit imperfections in both the source and detector. At the same time, the behavior of these imperfect devices is never exactly known due to characterization uncertainty, parameter fluctuations, and potential influence by an adversary. I...

Finite-Size Security of QKD: Comparison of Three Proof Techniques

We compare three proof techniques for composable finite-size security of quantum key distribution under collective attacks, with emphasis on how the resulting secret-key rates behave at practically relevant block lengths. As a benchmark, we consider the BB84 protocol and evaluate finite-size...