Formal Methods and Computer Security

Formal methods are variously considered to be arcane, tedious, and oblivious to practical concerns. However, such techniques as specification, type checking, proofs of correctness, and model checking, offer the power to analyze system properties under many or even infinitely many possible inputs and execution conditions without running an implemented system through all of the associated test cases. This talk will summarize some of the successful applications of formal methods for security problems such as protocol analysis, mobile code security, access control, and rights specifications.