Towards Model-Checking Quantum Security Protocols
Towards Model-Checking Quantum Security Protocols
复制标题
迈向模型检查量子安全协议
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
A. Sernadas
中科院分区：
文献类型：
--
作者：
Pedro Baltazar;Rohit Chadha;P. Mateus;A. Sernadas
关于量子态的推理逻辑已经在文献中给出。在本文中，我们扩展了一个这样的逻辑与时间结构模仿标准计算树逻辑用于推理经典转换系统。我们研究了这种时间量子逻辑的模型检查问题，并通过对BB84密钥分发协议的推理说明了它的使用。
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.