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. |
Year | DOI | Venue |
---|---|---|
2011 | 10.1007/978-3-642-25873-2_33 | OPODIS |
Keywords | Field | DocType |
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 | Two-phase commit protocol,Port Control Protocol,Computer science,Otway–Rees protocol,General Inter-ORB Protocol,Real-time computing,Internet Protocol Control Protocol,Internetwork protocol,Link Control Protocol,Distributed computing,Universal composability | Conference |
Volume | ISSN | Citations |
7109 | 0302-9743 | 1 |
PageRank | References | Authors |
0.36 | 13 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Petar Tsankov | 1 | 208 | 14.84 |
Mohammad Torabi | 2 | 301 | 31.19 |
David A. Basin | 3 | 4930 | 281.93 |