Abstract: Logics have had both direct and indirect roles in the modelling and analysis of secure systems, including operating systems and Internet protocols. Traditional mathematical logic supports the construction of general-purpose verification environments used in this area. Specialized modal logics have been used to model and verify authentication protocols and schemes for authentication and delegation using digital signature certificates.

Bio: Jonathan K. Millen, who received his Ph.D. from Rensselaer Polytechnic Institute in 1969, is a Senior Computer Scientist in the Computer Science Laboratory at SRI International. His research at SRI includes inductive methods for cryptographic protocol analysis, authentication protocol specification language design (CAPSL), and system survivability modelling. Before 1997 he worked in the Information Security Division of The MITRE Corporation, in computer security areas such as covert channel and information flow analysis, and protocol analysis. He supported the National Computer Security Center's Trusted Product Evaluation Program. Earlier interests include expert systems, automatic programming, and symbolic mathematical computation. Millen is co-editor-in-chief of the Journal of Computer Security, and a member of the editorial board of the ACM Transactions on Information and System Security. He is the founder and steering committee chair of the annual IEEE Computer Security Foundations Workshop. He has acted as general and program chair of that workshop and of the IEEE Symposium on Security and Privacy.