A Symbiotic Relationship Between Formal Methods and Security

Author: Jeannette M. Wing

Click here for the PostScript version.


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.