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.

The impact of this research will be varied and occur at different time scales. In the immediate future we anticipate a measurable output of new results and publications and a concomitant rise in activity in the topics addressed here. The effect of the research on dynamic epistemic logic and security will be directly linked to methods for producing highly assured software. Ultimately, guaranteeing the security of communication protocols is vital for the functioning of internet-based transactions. Of course, if we were to discover a flaw in any widely used protocol for privacy, anonymity or access control the impact would be immediate and dramatic. Finding such flaws is partly serendipity, which is not to deny the insight of people who have found such flaws; the point is that one cannot promise to reveal such major flaws. What this research can accomplish is to provide the framework to systematically check such protocols. It is a huge task of course and this project is not by itself going to solve it; it is, however, aimed at addressing a crucial piece of the task. The advanced educational impact of the visitor's presence in the U.K. will be immediate. He brings special expertise on the combination of logic and probability that is hard to duplicate. His presence in Oxford, the lectures that he will give there and the seminars that he will give throughout the U.K. will be a very tangible short-term effect of this project. The specific areas where he will be able to contribute will be quantum information theory to the Quantum Computation group at Oxford and the research groups at Edinburgh, Glasgow, Nottingham, York, Warwick and other places. His expertise in probabilistic reasoning will have impact on the probabilistic verification group headed by Prof. Kwaitkowska and other groups interested in probabilistic reasoning. The knowledge base of the U.K. research community will be immediately enhanced and there will be a significant contribution to the skills imparted to post-graduate students far out of proportion to the funding requested. The long range impact of probabilistic reasoning in general is potentially enormous. As embedded real-time systems become ubiquitous it will be necessary to approximate them with discrete models and automatically verify them. At this stage it will be absolutely crucial to be able to do this in a modular fashion, it will be crucial to model continuous systems and it will be crucial to reason probabilistically: these are precisely the features that distinguish of the visitor's research programme in probabilistic reasoning. Similarly, reasoning about quantum protocols is rapidly becoming vital. While communication based on quantum resources is still experimental, the experiments are showing that they are on the verge of becoming feasible. As we start to use quantum resources in protocols for secure communication we will need to understand the fundamental laws. At present, the community does not even have a clear notion of what knowledge means in a quantum setting. The impact of this part of the research will be significant for theory today and practice in the near future.