Constructing mid-points for two-party asynchronous protocols
PRINCIPLES OF DISTRIBUTED SYSTEMS(2011)
Abstract
Communication protocols describe the steps that the communication end-points must take in order to achieve a common goal. In practice, networks often contain mid-points, which can relay, redirect, or filter messages exchanged by the end-points. A mid-point can enforce a communication protocol: it forwards the messages that conform to the protocol, and drops them otherwise. Protocol specifications typically define only the end-points' behavior. Implementing a mid-point that enforces a protocol is nontrivial: the mid-point's behavior depends on the end-point's behavior, and also on the behavior of the communication environment in which the protocol executes. We present a process algebraic framework that takes as input the formal specifications of the protocol and the environment and outputs a specification for a mid-point that enforces the protocol. We prove that the mid-point specifications synthesized by our framework are correct: only messages that could have resulted from correctly executing end-points are forwarded. As an application, we construct a formal model for the mid-point that enforces the TCP three-way handshake protocol.
MoreTranslated text
Key words
process algebraic framework,constructing mid-points,common goal,communication protocol,two-party asynchronous protocol,formal specification,protocol specification,mid-point specification,formal model,communication environment,communication end-points,tcp three-way handshake protocol
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined