Logic and Information Flow in Classical and Quantum Systems

在安全应用程序中，代理希望在执行其正常功能的同时隐藏信息。这种隐藏敏感信息的能力必须保持，即使在恶意代理正在积极尝试查找机密信息的情况下也是如此。重要的是首先要理解对手知道某件事意味着什么。其次，重要的是量化对手知道多少信息，更重要的是，在攻击安全系统的过程中，对手能找到多少信息。当攻击者可以收集大量数据并对数据进行统计分析以尝试穿透安全屏障时，定量推理的重要性尤为重要。密码学家破译密码的能力很大程度上依赖于统计分析。最早的密码在今天很容易破解，只要简单地分析一下被编码的语言中哪些字母最常见。如今，有了不易破解的复杂密码，更令人兴奋的是，量子力学的基本定律可以保护秘密。当然，即使有好的密码，当用于执行安全任务的协议中存在逻辑缺陷时，安全系统中也可能存在漏洞。拟议中的研究有三个主要重点。首先，我们想要理解知识在量子环境中究竟意味着什么。在这里，人们必须解决位于逻辑和物理学边界上的基本问题。其次，我们想量化量子系统中的知识，并推理知识如何作为代理遵循一些固定的协议来确保安全。最后，我们希望开发一个干净的逻辑框架，它最终可以用作自动检查协议正确性的基础。我们所考虑的应用与目前正在使用的协议有关，例如电子商务，以及基于量子力学的其他通信协议。后者尚处于实验阶段，但可以在实践中部署此类系统的时间正在接近。

In security applications an agent wants to conceal information while proceeding with its normal functioning. This ability to conceal sensitive information must hold even in the presence of malicious agents that are actively trying to find out secret information. It is important to understand first of all what it means for an adversary to know something. Secondly it is important to quantify how much an adversary knows and even more importantly how much information an adversary can find out during its attempts to attack a security system. The importance of reasoning quantitatively is particularly important when the adversary can collect large quantities of data and perform statistical analysis of the data to try and penetrate security barriers. The ability of cryptographers to break cyphers largely rests on statistical analysis. The earliest cyphers are easily broken today by simple analysis of which letters are most common in the language being encoded. Now days, there are sophisticated cyphers that cannot be broken easily and even more exciting prospects of secrets being protected by the fundamental laws of quantum mechanics. Of course, even with good cyphers there may be breaches in secure systems when there are logical flaws in the protocols that are used for performing security tasks. The proposed research has three main thrusts. First of all we would like to understand what knowledge even means in a quantum setting. Here one has to tackle fundamental questions that lie at the boundary of logic and physics. Second, we would like to quantify knowledge in quantum systems and reason about how knowledge flows as agents follow some fixed protocols to ensure security. Finally, we would like to develop a clean logical framework that can be ultimately used as the basis for automatically checking the correctness of protocols. The applications that we have in mind relate to protocols currently in use for example in electronic commerce and also other protocols for communication based on quantum mechanics. The latter are in the experimental stage but the time is coming close where such systems could be deployed in practice.