Title :
Towards Model-Checking Quantum Security Protocols
Author :
Baltazar, P. ; Chadha, R. ; Mateus, P. ; Sernadas, A.
Author_Institution :
SQIG-IT, Lisbon
Abstract :
Logics for reasoning about quantum states have been given in the literature. In this paper, we extend one such logic with temporal constructs mimicking the standard computational tree logic used to reason about classical transition systems. We investigate the model-checking problem for this temporal quantum logic and illustrate its use by reasoning about the BB84 key distribution protocol.
Keywords :
cryptographic protocols; quantum cryptography; BB84 key distribution protocol; classical transition systems; computational tree logics; model-checking quantum security protocols; quantum logics; Cost accounting; Hilbert space; Information processing; Information security; Logic design; Measurement standards; Protocols; Quantum computing; Quantum mechanics; Tensile stress;
Conference_Titel :
Quantum, Nano, and Micro Technologies, 2007. ICQNM '07. First International Conference on
Conference_Location :
Guadeloupe City
Electronic_ISBN :
0-7695-2759-0
DOI :
10.1109/ICQNM.2007.21
