Towards Improved Logics For Reasoning About Security

点击翻译按钮获取中文摘要

Security protocols are notoriously difficult to design and prove correct. The goal of this project is to design a logic that deals with a number of deficiencies in current logics. The focus will be on two issues: (1) Getting more realistic notions of knowledge: Informal arguments regarding the correctness of security protocols often involve statements about knowledge and belief. Assumptions such as "The adversary does not know the key" and "The participants believe that k is a good session key" are standard. The standard semantics for these operators has the problem that agents are able to deduce all logical tautologies and the logical consequences of their knowledge. Because agents "know" how to factor, for example, they can break RSA.(2) Modeling more general intruders: Current logics almost invariably use the Dolev-Yao intruder model, which assume that an intruder can compose messages, replay them, or decipher them if she knows the right keys, but cannot otherwise "crack" encrypted messages. While useful, this model is restrictive, in that it does not consider the knowledge that agents have of the protocol being run and cannot deal with probabilistic arguments, such as an adversary randomly guessing the right key to use. The research will take as its point of departure the standard models of knowledge and belief based on possible worlds, augmented with probability, so as to be able to reason about knowledge and probability. The notion of algorithmic knowledge, where an agent uses an algorithm to compute what it knows, will be used to deal with resource-bounded reasoning.