License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2015.441
URN: urn:nbn:de:0030-drops-53936
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5393/
Go to the corresponding LIPIcs Volume Portal

Feng, Yuan ; Ying, Mingsheng

Toward Automatic Verification of Quantum Cryptographic Protocols

pdf-format:
33.pdf (0.5 MB)

Abstract

Several quantum process algebras have been proposed and successfully applied in verification of quantum cryptographic protocols. All of the bisimulations proposed so far for quantum processes in these process algebras are state-based, implying that they only compare individual quantum states, but not a combination of them. This paper remedies this problem by introducing a novel notion of distribution-based bisimulation for quantum processes. We further propose an approximate version of this bisimulation that enables us to prove more sophisticated security properties of quantum protocols which cannot be verified using the previous bisimulations. In particular, we prove that the quantum key distribution protocol BB84 is sound and (asymptotically) secure against the intercept-resend attacks by showing that the BB84 protocol, when executed with such an attacker concurrently, is approximately bisimilar to an ideal protocol, whose soundness and security are obviously guaranteed, with at most an exponentially decreasing gap.

BibTeX - Entry

@InProceedings{feng_et_al:LIPIcs:2015:5393,
  author =	{Yuan Feng and Mingsheng Ying},
  title =	{{Toward Automatic Verification of Quantum Cryptographic Protocols}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{441--455},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Luca Aceto and David de Frutos Escrig},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5393},
  URN =		{urn:nbn:de:0030-drops-53936},
  doi =		{10.4230/LIPIcs.CONCUR.2015.441},
  annote =	{Keywords: Quantum cryptographic protocols, Verification, Bisimulation, Security}
}

Keywords: Quantum cryptographic protocols, Verification, Bisimulation, Security
Collection: 26th International Conference on Concurrency Theory (CONCUR 2015)
Issue Date: 2015
Date of publication: 26.08.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI