Reasoning about Security Protocols
Abstract. Security protocols, as used in distributed systems for authentication
and related purposes, are notoriously prone to failures. Therefore,
over time, various methods have been developed for the design and
analysis of these protocols. This tutorial describes calculi for
reasoning about security protocols, in particular an extension of the
pi calculus with function symbols that can represent cryptographic
operations. It also explains some techniques and tools for protocol
analysis, focusing on Blanchet's tool ProVerif.
ProVerif and some related papers can be found at http://www.di.ens.fr/~blanchet/crypto-eng.html. Additional papers are at http://www.cs.ucsc.edu/~abadi/allpapers.html.
Description Logic Reasoning
Abstract. Description Logics (DLs) are a family of logic based knowledge representation formalisms. Although they have a range of applications (e.g., configuration and information integration), they are perhaps best known as the basis for widely used ontology languages such as OWL (now a W3C recommendation). This decision was motivated by a requirement that key inference problems be decidable, and that it should be possible to provide reasoning services to support ontology design and deployment. Such reasoning services are typically provided by highly optimised implementations of tableaux decision procedures. In this tutorial we will study both the logics and decision procedures that underpin modern ontology languages, and the implementation techniques that have enabled state of the art systems to be effective in applications in spite of the high worst case complexity of key inference problems.