Computer Science Department
School of Computer Science, Carnegie Mellon University


A Symbiotic Relationship Between Formal Methods and Security

Jeannette M. Wing

December 1998

This paper will appear in an edited volume resulting from the series of two workshops held in 1998, sponsored by the ONR and HSF, entitled
Workshops on Computer Security, Fault Tolerance, and Software Assurance: From Needs to Solutions

Keywords: Formal methods, specification, verification, model checking, theorem proving, security, authentication, electronic commerce

Security played a significant role in the development of formal methods in the 70s and early 80s. Have the tables turned? Are formal methods now ready to play a significant role in the development of more secure systems? While not a panacea, the answer is yes, formal methods can and should play such a role. In this paper I first review the limits of formal methods. Then after a brief historical excursion, I summarize some recent results on how model checking and theorem proving tools revealed new and known flaws in authentication protocols. Looking to the future I discuss the challenges and opportunities for formal methods in analyzing the security of systems, above and beyond the protocol level.

13 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by