A Framework For Model Checking Object Oriented Security Protocol Implementations

With the rapid growth of the Internet, more and more vendors see the Internet as a viable marketplace. Since the Internet is public, providing security in the presence of malicious intruders has become paramount. Security protocols have been proposed to protect systems. These protocols work by exchanging messages, many of which are encrypted. Though it may take a long time for an intruder to break the underlying encryption employed by the protocol, it is possible for the intruder to intervene in the authentication process. It may take years before a crucial loophole is discovered in a security protocol. Until then, its implementation may remain in use. There are several methods for verifying security protocols from their specifications. A specification that is successfully verified for some properties does not imply that the implementation created from it will also satisfy those properties. In this paper, we show a framework for model checking object oriented implementations of security protocols. According to this framework, we reverse engineer security protocol implementations to UML sequence diagrams for a particular use case. The sequence diagrams are then converted to state machines for each principal participating in the use case. The state machine of each principal is used to generate its Promela model. Promela is the language used by the SPIN model checker. Once we have a Promela model for each principal involved in the use case, we can use the SPIN model checker to check if a particular property is satisfied. As a case study, we use an implementation of the NSPK protocol and check if the implementation satisfies the property of authenticity. We conclude by showing that the implementation is prone to an attack from an intruder and that the property of authenticity is violated.