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.