Protocol Verification via Projections

TLDR

A protocol system is a network of entities communicating over channels, where messages can be lost, duplicated, or reordered. The authors introduce a projection method that reduces the complexity of analyzing complex communication protocols by constructing image protocols for each function. Image protocols are specified like real protocols and are constructed using two illustrative examples to demonstrate the method. Image protocols are faithful, preserving safety and liveness, smaller, and easier to analyze, as shown on an HDLC protocol in a companion paper.

Abstract

The method of projections is a new approach to reduce the complexity of analyzing nontrivial communication protocols. A protocol system consists of a network of protocol entities and communication channels. Protocol entities interact by exchanging messages through channels; messages in transit may be lost, duplicated as well as reordered. Our method is intended for protocols with several distinguishable functions. We show how to construct image protocols for each function. An image protocol is specified just like a real protocol. An image protocol system is said to be faithful if it preserves all safety and liveness properties of the original protocol system concerning the projected function. An image protocol is smaller than the original protocol and can typically be more easily analyzed. Two protocol examples are employed herein to illustrate our method. An application of this method to verify a version of the high-level data link control (HDLC) protocol is described in a companion paper.