A Framework For Model Checking Object Oriented Security Protocol Implementations
| Title: | A Framework For Model Checking Object Oriented Security Protocol Implementations |
| Author: | Singh, Parikshit |
| Abstract: | 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 . |
| URI: |
http : / /hdl .handle .net /10106 /531
http : / /hdl .handle .net /10106 /531 |
| Date: | 2007-08-23 |
Citation
(June 2005).
A Framework For Model Checking Object Oriented Security Protocol Implementations.
University of Texas at Arlington. Available electronically from
http : / /hdl .handle .net /10106 /531
.
Files in this item
| Files | Size | Format | View |
|---|---|---|---|
| umi-uta-1004.pdf | 686.0Kb | application/pdf |
View/ |