A compositional logic for protocol correctness
A compositional logic for protocol correctness
复制标题
协议正确性的组合逻辑
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Dusko Pavlovic
中科院分区：
文献类型：
--
作者：
N. Durgin;John C. Mitchell;Dusko Pavlovic
摘要：我们提出了一种专门的协议逻辑，它是围绕过程语言构建的，用于描述协议的操作。一般来说，逻辑和协议之间的关系就像 Floyd-Hoare 逻辑中的断言和标准命令式程序之间的关系。与 Floyd-Hoare 逻辑一样，我们的逻辑包含每个主要协议操作的公理和推理规则，并且证明是协议导向的，这意味着正确性证明的轮廓遵循协议中的操作序列。我们证明协议逻辑在特定意义上是合理的：关于一个动作或动作序列的每个可证明的断言在协议的任何运行中都成立，受到攻击，其中发生给定的动作。这种方法使我们能够证明在所有运行中都适用的协议属性，同时仅显式推理实现该属性所需的操作序列。特别是，不需要对攻击者的潜在行为进行明确的推理。
Abstract: We present a specialized protocol logic that is built around a process language for describing the actions of a protocol. In general terms, the relation between logic and protocol is like the relation between assertions in Floyd-Hoare logic and standard imperative programs. Like Floyd-Hoare logic, our logic contains axioms and inference rules for each of the main protocol actions and proofs are protocol-directed, meaning that the outline of a proof of correctness follows the sequence of actions in the protocol. We prove that the protocol logic is sound, in a specific sense: each provable assertion about an action or sequence of actions holds in any run of the protocol, under attack, in which the given actions occur. This approach lets us prove properties of protocols that hold in all runs, while explicitly reasoning only about the sequence of actions needed to achieve this property. In particular, no explicit reasoning about the potential actions of an attacker is required.