LPAR 2004 Tutorial Program


Martín Abadi (University of California at Santa Cruz)

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.


Ian Horrocks (University of Manchester)

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.