Towards Improved Logics For Reasoning About Security

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

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.