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

• Thomas Y. C. Woo and Simon S. Lam, A Semantic Model for Authentication Protocols, Proceedings IEEE Symposium on Research in Security and Privacy, Oakland, May 1993.
• Thomas Y. C. Woo and Simon S. Lam, Design, Verification and Implementation of an Authentication Protocol, Proc. Int. Conference on Network Protocols, Boston, October 1994.
• Thomas Y. C. Woo and Simon S. Lam, Verifying Authentication Protocols: Methodology and Example, Proceedings International Conference on Network Protocols, San Francisco, October 1993.
• Simon S. Lam, A. Udaya Shankar, and Thomas Y. C. Woo, Applying a Theory of Modules and Interfaces to Security Verification, Proceedings IEEE Symposium on Research in Security and Privacy, Oakland, May 1991.

Interface semantics

• Simon S. Lam and A. Udaya Shankar, A Theory of Interfaces and Modules I--Composition Theorem, IEEE Transactions on Software Engineering, vol. 20, no. 1, pages 55-71, January 1994  (more info).
• Simon S. Lam and A. Udaya Shankar, Specifying Modules to Satisfy Interfaces: A State Transition System Approach, Distributed Computing, July 1992.
• Simon S. Lam and A. Udaya Shankar, Understanding Interfaces, Proceedings Fourth International Conference on Formal Description Techniques, Sydney, Australia, November 1991. (Conference Keynote Address)

Projection and refinement mappings

• Simon S. Lam and A. Udaya Shankar, Protocol Verification via Projections, IEEE Transactions on Software Engineering, Vol. SE-10, No. 4, July 1984.  
• Simon S. Lam and A. Udaya Shankar, A Relational Notation for State Transition Systems, IEEE Transactions on Software Engineering, vol. 16, no. 7, pages 755-775, July 1990 (more info).
• Simon S. Lam and A. Udaya Shankar, Refinement and Projection of Relational Specifications, in Stepwise Refinement of Distributed Systems, J. W. de Bakker, W. P. de Roever and G. Rozenberg (editors), Lecture Notes in Computer Science 430, Springer-Verlag, May 1990.

Application to multifunction protocols

• A. Udaya Shankar and Simon S. Lam, A Stepwise Refinement Heuristic for Protocol Construction, ACM TOPLAS, vol. 14, no. 3, pages 417-461, July 1992 (more info).
• C. H. Chow, Mohamed G. Gouda, and Simon S. Lam, A Discipline for Constructing Multiphase Communication Protocols, ACM Transactions on Computer Systems, Vol. 3, No. 4, November 1985.
• A. Udaya Shankar and Simon S. Lam, An HDLC Protocol Specification and its Verification Using Image Protocols, ACM Transactions on Computer Systems, Vol. 1, No. 4, pp. 331-368, November 1983.

Protocol conversion

• Simon S. Lam, Protocol Conversion, IEEE Transactions on Software Engineering, Vol. 14, No. 3, March 1988; correction in IEEE Transactions on Software Engineering, Vol. 14, No. 9, Sept. 1988, page 1376. 
• Kenneth L. Calvert and Simon S. Lam, Formal Methods for Protocol Conversion, IEEE Journal on Selected Areas in Communications, Vol. 8, No. 1, January 1990.
• Kenneth L. Calvert and Simon S. Lam, Adaptors for Protocol Conversion, Proceedings INFOCOM '90, San Francisco, June 1990.
• Kenneth L. Calvert and Simon S. Lam, Deriving a Protocol Converter: A Top-Down Method, Proceedings ACM SIGCOMM Symposium, Austin, Texas, September 1989.
• Kenneth L. Calvert and Simon S. Lam, An Exercise in Deriving a Protocol Conversion, Proceedings ACM SIGCOMM, Stowe, VT, August 1987.
• Simon S. Lam, Protocol Conversion--Correctness Problems, Proceedings ACM SIGCOMM, Stowe, VT, August 1986.

Real-time protocols and properties

• A. Udaya Shankar and Simon S. Lam, Time-Dependent Distributed Systems: Proving Safety, Liveness, and Real-Time Properties, Distributed Computing, Vol. 2, 1987.
• Pradeep Jain and Simon S. Lam, Specification of Real-Time Broadcast Networks, IEEE Transactions on Computers, Vol. 40, No. 4, April 1991.
• Pradeep Jain and Simon S. Lam, Modeling and Verification of Real-Time Protocols for Broadcast Networks, IEEE Transactions on Software Engineering, Vol. SE-13, No. 8, August 1987.