Simon S. Lam (more
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.
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.
Thereafter, quite a bit of work followed on automatic checking of security protocol properties based upon state transition semantics.