Towards Model-Checking Quantum Security Protocols
Pedro Baltazar, Rohit Chadha, Paulo Mateus, Amı́lcar Sernadas · 2007
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.