Accession Number : ADA327281

Title :   Model Checking for Security Protocols,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Marrero, Will ; Clarke, Edmund ; Jha, Somesh

PDF Url : ADA327281

Report Date : MAY 1997

Pagination or Media Count : 20

Abstract : As more resources are added to compiler networks and as more vendors look to the World Wide Web as a viable marketplace the importance of being able to restrict access and to insure some kind of acceptable behavior even in the presence of malicious intruders becomes paramount. People have looked to cryptography to help solve many of these problems. However cryptography itself is only a tool. The security of a system depends not only on the cryptosystem being used but also on how it is used. Typically researchers have proposed the use of Security protocols to provide these security guarantees. These protocols consist of a sequence of messages - many with encrypted parts. In this paper we develop a way of verifying these protocols using model checking. Model checking has proven to be a very useful technique for verifying hardware designs. By modeling circuits as finite state machines and examining all possible execution traces modeling has found a number of errors in real world designs. Like hardware designs security protocols are very subtle and can also have bugs which are difficult to find.

Descriptors :   *DATA PROCESSING SECURITY, *COMPILERS, GLOBAL, CRYPTOGRAPHY, GUARANTEES, ERRORS, MACHINES, COMPUTER NETWORKS.

Subject Categories : Computer Programming and Software
      Computer Systems Management and Standards

Distribution Statement : APPROVED FOR PUBLIC RELEASE