# Graphical Methods in Device-Independent Quantum Cryptography

## TL;DR

This paper presents a new graphical framework based on categorical quantum mechanics to simplify and automate security proofs in device-independent quantum cryptography, demonstrated through reproofs and proof assistant implementation.

## Contribution

It introduces a novel graphical approach for security proofs in quantum cryptography, making complex proofs more accessible and enabling automation.

## Key findings

- Reproved a key result: linear to unbounded randomness expansion.
- Developed a graphical proof framework for quantum cryptography.
- Implemented proof verification in Globular proof assistant.

## Abstract

We introduce a framework for graphical security proofs in device-independent quantum cryptography using the methods of categorical quantum mechanics. We are optimistic that this approach will make some of the highly complex proofs in quantum cryptography more accessible, facilitate the discovery of new proofs, and enable automated proof verification. As an example of our framework, we reprove a previous result from device-independent quantum cryptography: any linear randomness expansion protocol can be converted into an unbounded randomness expansion protocol. We give a graphical proof of this result, and implement part of it in the Globular proof assistant.