Paper Info
Title
Applying Formal Methods to an Information Security Device: An Experience Report
Abstract
SCR (Software Cost Reduction) is a formal method for specifying and analyzing system requirements that has previously been applied to control systems. This paper describes a case study in which the SCR method was used to specify and analyze a different class of system, a cryptographic system called CD, which must satisfy a large set of security properties. The paper describes how a suite of tools supporting SCR a consistency checker, simulator, model checker, invariant generator, theorem prover, and validity checker were used to detect errors in the SCR specification of CD and to verify that the specification satisfies seven security properties. The paper also describes issues of concern to software developers about formal methods, e.g., ease of use, cost-effectiveness, scalability, how to translate a prose specification into a formal notation, and what process to follow in applying a formal method and discusses these issues based on our experience with CD. Also described are some unexpected results of our case study.
Year
DOI
Venue
1999
10.1109/HASE.1999.809478
HASE
Keywords
Field
DocType
system requirements,security,systems analysis,scaling factor,theorem proving,cryptography,simulators,theorem prover,information security,formal method,simulator,application software,thyristors,control systems,simulation model,model checker,formal methods,software engineering,formal specification,control system,error correction,scalability,analyzers
Programming language,Model checking,Software engineering,Computer science,Systems analysis,Information security,Formal specification,Software,Formal methods,System requirements,Application software,Reliability engineering
Conference
ISBN
Citations 
PageRank 
0-7695-0418-3
8
0.78
References 
Authors
5
3
Name
Order
Citations
PageRank
James Kirby, Jr.1529.40
Myla Archer246356.43
Constance L. Heitmeyer3898151.71