Thursday, October 24, 2019
Alexandru Dragomir (University of Bucharest)
An introduction to BAN logic (a logic of authentication)
Abstract: One of the first and most discussed logical approaches to the problem of verifying security protocols is the one proposed in BAN logic (Burrows, Abadi \& Needham 1989). BAN logic is a many-sorted modal logic used for its intuitive and compelling set of inference rules devised for reasoning about an agentís beliefs, trust and message exchange. My presentation will focus on (1) presenting the language and inference rules of BAN logic, (2) following the original paper's analysis of the Otway-Rees protocol, (3) presenting some objections to using BAN, and (4) discussing the problem of offering a semantics of BAN logic.
Thursday, September 19, 2019 in Hall 214
Radu Iosif (CNRS - VERIMAG, France) )
Checking Deadlock Freedom of Component-based Systems
Abstract: We consider concurrent systems consisting of a finite but unknown number of components, that are replicated instances of a given set of finite state automata. The components communicate by executing interactions which are simultaneous atomic state changes of a set of components. We specify both the type of interactions (e.g. rendez-vous, broadcast) and the topology (i.e. architecture) of the system (e.g. pipeline, ring) via a decidable interaction logic, which is embedded in the classical weak sequential calculus of one successor (WS1S). Proving correctness of such system for safety properties, such as deadlock freedom or mutual exclusion, requires the inference of an inductive invariant that subsumes the set of reachable states and avoids the unsafe states. Our method synthesizes such invariants directly from the formula describing the interactions, without costly fixed point iterations. We applied our technique to the verification of several textbook examples, such as dining philosophers, mutual exclusion protocols and concurrent systems with preemption and priorities.
Joint work with Marius Bozga and Joseph Sifakis.