University of Texas at Austin Department of Computer Sciences Networking Research Laboratory
Department of Computer Sciences
The University of Texas at Austin

Director: Simon S. Lam (more publications)

Protocol Specification and Verification

In the 1980s, we observed that a data link (or transport layer) protocol typically performs multiple functions.  This observation led us to ask some fundamental questions, such as:  What is meant by protocol A being an abstraction of protocol B ? What is meant by protocol B being a refinement of protocol A ?  Our answers to these questions gave rise to efficient methods for the design and verification of multifunction protocols.  We first developed a method called protocol projections.  Using this method, several image protocols are first constructed from a given protocol, such that progress and safety properties of each image protocol are also properties of the given protocol.  The projection mapping from a protocol to an image protocol made us think about the refinement mapping from a simple protocol to a more detailed protocol.  We developed a theory of refinement and then a stepwise refinement methodology for the construction of nontrivial protocols. With these methods, we were the first to formally specify and verify correctness properties of the HDLC protocol and the sliding window protocol (used in TCP). 

We then developed a theory of modules and interfaces in which a system is modeled as a directed acyclic graph where nodes represent modules and arcs represent interfaces. At the heart of our theory is a definition of what it means for a module to satisfy a set of interfaces, as a service provider for some and as a service consumer for others. Our definition of interface satisfaction is designed to be separable, i.e., interfaces encode adequate information such that each module in a system can be designed and verified separately, and composable, i.e., we have proved a composition theorem for the system model in general.

Furthermore, we made seminal contributions towards formalization of the protocol conversion problem and developed methods for deriving converters/adaptors to achieve interoperability between different protocol implementations.  We also developed models and methods for specifying and proving real-time properties.

In the early 1990s, we developed  a formal model and methodology for verifying security protocols based upon state transition semantics. We used them to specify and verify a client-server authentication protocol.  Our model was later used by Clarke's group at CMU to develop a model checker for security protocols. 

Selected Publications

Security and authentication protocols

Interface semantics

Projection and refinement mappings

Application to multifunction protocols

Protocol conversion

Real-time protocols and properties