A symbiotic relationship between formal methods and security

Author

Wing, Jeannette M.

Author_Institution

Sch. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA

fYear

1998

fDate

1998

Firstpage

26

Lastpage

38

Abstract

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 we first review the limits of formal methods. Then after a brief historical excursion, we summarize some recent results on how model checking and theorem proving tools revealed new and known flaws in authentication protocols. Looking to the future we discuss the challenges and opportunities for formal methods in analyzing the security of systems, above and beyond the protocol level

Keywords

formal verification; message authentication; protocols; theorem proving; authentication protocols; formal methods; model checking; security; symbiotic relationship; theorem proving; Authentication; Computer science; Computer security; Government; Internet; National security; Operating systems; Protocols; Research and development; Symbiosis;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Security, Dependability and Assurance: From Needs to Solutions, 1998. Proceedings

Conference_Location

York, UK ; Williamsburg, VA

Print_ISBN

0-7695-0337-3

Type

conf

DOI

10.1109/CSDA.1998.798355

Filename

798355