Towards Improved Logics For Reasoning About Security

众所周知，安全协议很难设计和证明是正确的。这个项目的目标是设计一种处理当前逻辑中的一些缺陷的逻辑。重点将放在两个问题上：(1)获得更现实的知识概念：关于安全协议正确性的非正式争论通常涉及关于知识和信念的陈述。诸如“对手不知道密钥”和“参与者认为k是一个好的会话密钥”之类的假设是标准的。这些运算符的标准语义存在一个问题，即代理能够推导出所有逻辑重言式及其知识的逻辑结果。因为代理知道如何分解，例如，他们可以破解RSA。(2)对更一般的入侵者进行建模：当前的逻辑几乎总是使用Dolev-姚入侵者模型，该模型假设入侵者可以编写消息、重放消息或解密消息(如果她知道正确的密钥)，但不能以其他方式“破解”加密消息。虽然有用，但该模型是受限的，因为它不考虑代理对正在运行的协议的了解，并且不能处理概率参数，例如对手随机猜测要使用的正确密钥。这项研究将以可能世界为基础的知识和信念的标准模型为出发点，并以概率为补充，从而能够对知识和概率进行推理。算法知识的概念，其中代理使用算法来计算它所知道的，将被用于处理资源受限的推理。

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.