# QKD in Isabelle -- Bayesian Calculation

## TL;DR

This paper formalizes the security proof of Quantum Key Distribution in Isabelle, focusing on probabilistic reasoning to demonstrate that an adversary cannot be certain of the key bits before comparison.

## Contribution

It introduces a formal probabilistic framework in Isabelle for QKD, providing a rigorous proof of the core security argument.

## Key findings

- Formal proof of QKD security in Isabelle
- Graphical depiction of protocol steps and probabilities
- Probabilistic reasoning demonstrating adversary uncertainty

## Abstract

In this paper, we present a first step towards a formalisation of the Quantum Key Distribution algorithm in Isabelle. We focus on the formalisation of the main probabilistic argument why Bob cannot be certain about the key bit sent by Alice before he does not have the chance to compare the chosen polarization scheme. This means that any adversary Eve is in the same position as Bob and cannot be certain about the transmitted keybits. We introduce the necessary basic probability theory, present a graphical depiction of the protocol steps and their probabilities, and finally how this is translated into a formal proof of the security argument.