Semi-automated verification of security proofs of quantum cryptographic protocols

This paper presents a formal framework for semi-automated verification of security proofs of quantum cryptographic protocols. We simplify the syntax and operational semantics of quantum process calculus qCCS so that verification of weak bisimilarity of configurations becomes easier. In addition, we...

Full description

Saved in:
Bibliographic Details
Published in:Journal of symbolic computation 2016-03, Vol.73, p.192-220
Main Authors: Kubota, Takahiro, Kakutani, Yoshihiko, Kato, Go, Kawano, Yasuhito, Sakurada, Hideki
Format: Article
Language:English
Subjects:
Formal methods
Process calculi
Quantum key distribution
Quantum protocols
Semi-automated verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper presents a formal framework for semi-automated verification of security proofs of quantum cryptographic protocols. We simplify the syntax and operational semantics of quantum process calculus qCCS so that verification of weak bisimilarity of configurations becomes easier. In addition, we generalize qCCS to handle security parameters and quantum states symbolically. We then prove the soundness of the proposed framework. A software tool, named the verifier, is implemented and applied to the verification of Shor and Preskill's unconditional security proof of BB84. As a result, we succeed in verifying the main part in Shor and Preskill's unconditional security proof of BB84 against an unlimited adversary's attack semi-automatically, i.e., it is automatic except for giving user-defined equations.
ISSN:0747-7171
1095-855X
DOI:10.1016/j.jsc.2015.05.001