Director: Simon S. Lam (more publications)

A formal model for verifying security protocols

When we first started thinking about how to verify some authentication protocols we had designed, several logics were available in which one could express and deduce security properties. The most prominent example was BAN logic. While BAN logic had been used to uncover various protocol weaknesses, it was also criticized for its high level of abstraction and its need for a protocol idealization step. Specifically, the user is required to transform each message in a protocol into formulas about the message. This step could be a source of problems.

My former student, Thomas Woo, and I decided to use a much more intuitive approach to model security protocols. We model protocol entities as communicating processes that exchange encrypted and unencrypted messages. Reasoning about correctness is based upon the set of all execution sequences. Though this sounds straightforward, it was not easy to accomplish as considerable insight was needed to model protocol states and state transitions, and then come up with the right assertions for security protocols. We found two classes of assertions (called secrecy and correspondence properties) that are appropriate for security protocols, and we provided proof rules for verifying them. Our proof rules are similar to those in temporal logic.

• A semantic model for authentication protocols
  Thomas Y. C. Woo and Simon S. Lam
  Proc. IEEE Symposium on Research in Security and Privacy, Oakland, May 1993 (postscript file).
  
  
• Verifying authentication protocols: Methodology and example
  Thomas Y. C. Woo and Simon S. Lam
  Proc. IEEE Int. Conference on Network Protocols, San Francisco, October 1993 (postscript file).

When Ed Clarke visited our department in 1996, I talked to him about network security research and showed him our papers on authentication protocol verification. I conjectured that since reasoning in our formal model was based upon state transition semantics (set of all execution traces), model checking could be used to check our security properties. With our model as the basis, Clarke's group developed a model checker for security protocols several months later.

• A model checker for security protocols
  W. Marrero, E. M. Clarke, and S. Jha
  DIMACS Workshop on Design and Formal Verification of Security Protocols 1997. A preliminary version appeared as technical report TR-CMU-CS-97-139, Carnegie Mellon University, May 1997.

Thereafter, quite a bit of work followed on automatic checking of security protocol properties based upon state transition semantics.