Toward automatic verification of quantum cryptographic protocols

Feng, Y; Ying, M

Toward automatic verification of quantum cryptographic protocols

Feng, Y

Ying, M

Permalink

Publication Type:: Conference Proceeding
Citation:: Leibniz International Proceedings in Informatics, LIPIcs, 2015, 42 pp. 441 - 455
Issue Date:: 2015-08-01

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download Accepted Manuscript versionAdobe PDF (579.58 kB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Feng, Y https://orcid.org/0000-0002-3097-3896	en_US
dc.contributor.author	Ying, M https://orcid.org/0000-0003-4847-702X	en_US
dc.date.issued	2015-08-01	en_US
dc.identifier.citation	Leibniz International Proceedings in Informatics, LIPIcs, 2015, 42 pp. 441 - 455	en_US
dc.identifier.isbn	9783939897910	en_US
dc.identifier.issn	1868-8969	en_US
dc.identifier.uri	http://hdl.handle.net/10453/41921
dc.description.abstract	© Yuan Feng and Mingsheng Ying; licensed under Creative Commons License CC-BY. 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.	en_US
dc.relation	http://purl.org/au-research/grants/arc/DP160101652
dc.relation	http://purl.org/au-research/grants/arc/DP130102764
dc.relation.ispartof	Leibniz International Proceedings in Informatics, LIPIcs	en_US
dc.relation.isbasedon	10.4230/LIPIcs.CONCUR.2015.441	en_US
dc.title	Toward automatic verification of quantum cryptographic protocols	en_US
dc.type	Conference Proceeding
utslib.citation.volume	42	en_US
utslib.for	010503 Mathematical Aspects of Classical Mechanics, Quantum Mechanics and Quantum Information Theory	en_US
utslib.for	080203 Computational Logic and Formal Languages	en_US
pubs.embargo.period	Not known	en_US
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Strength - QSI - Centre for Quantum Software and Information
utslib.copyright.status	open_access
pubs.publication-status	Published	en_US
pubs.volume	42	en_US

Abstract:

© Yuan Feng and Mingsheng Ying; licensed under Creative Commons License CC-BY. 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.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/41921