dorsal/arxiv
View SchemaFormal Verification of Quantum Protocols
| Authors | Rajagopal Nagarajan, Simon Gay |
|---|---|
| Categories | |
| ArXiv ID | quant-ph/0203086 |
| URL | https://arxiv.org/abs/quant-ph/0203086 |
Abstract
We propose to analyse quantum protocols by applying formal verification techniques developed in classical computing for the analysis of communicating concurrent systems. One area of successful application of these techniques is that of classical security protocols, exemplified by Lowe's discovery and fix of a flaw in the well-known Needham-Schroeder authentication protocol. Secure quantum cryptographic protocols are also notoriously difficult to design. Quantum cryptography is therefore an interesting target for formal verification, and provides our first example; we expect the approach to be transferable to more general quantum information processing scenarios. The example we use is the quantum key distribution protocol proposed by Bennett and Brassard, commonly referred to as BB84. We present a model of the protocol in the process calculus CCS and the results of some initial analyses using the Concurrency Workbench of the New Century (CWB-NC).
{
"annotation_id": "6cce7833-78f8-4705-b33d-616ac91f8084",
"date_created": "2026-03-02T18:01:49.153000Z",
"date_modified": "2026-03-02T18:01:49.153000Z",
"file_hash": "fa498e4d2bea0b06b031a802815b5546a9b8ece14cdc0d3279b9bfe64c8434a8",
"private": false,
"record": {
"abstract": "We propose to analyse quantum protocols by applying formal verification\ntechniques developed in classical computing for the analysis of communicating\nconcurrent systems. One area of successful application of these techniques is\nthat of classical security protocols, exemplified by Lowe\u0027s discovery and fix\nof a flaw in the well-known Needham-Schroeder authentication protocol. Secure\nquantum cryptographic protocols are also notoriously difficult to design.\nQuantum cryptography is therefore an interesting target for formal\nverification, and provides our first example; we expect the approach to be\ntransferable to more general quantum information processing scenarios. The\nexample we use is the quantum key distribution protocol proposed by Bennett and\nBrassard, commonly referred to as BB84. We present a model of the protocol in\nthe process calculus CCS and the results of some initial analyses using the\nConcurrency Workbench of the New Century (CWB-NC).",
"arxiv_id": "quant-ph/0203086",
"authors": [
"Rajagopal Nagarajan",
"Simon Gay"
],
"categories": [
"quant-ph"
],
"title": "Formal Verification of Quantum Protocols",
"url": "https://arxiv.org/abs/quant-ph/0203086"
},
"schema_id": "dorsal/arxiv",
"source": {
"execution_id": "06c36b3b-a567-41c5-a5d7-92c6a9ffc120",
"id": "arXiv Dataset IDs",
"type": "Model",
"variant": "snapshot-2026-03-01",
"version": "0.1.0"
},
"user_id": 1000002
}