**David Basin**, ETH Zurich

Title: *Cryptographically Sound Protocol-Model Abstractions*

**Martin Grohe**, Humboldt University Berlin

Title: *The Quest for a Logic Capturing PTIME*

**Dexter Kozen**, Cornell University

Title: *Nonlocal Flow of Control and Kleene Algebra with Tests*

**Yiannis Moschovakis**, UCLA and University of Athens

Title: *The Axiomatic Derivation of Absolute Lower Bounds*

**David Basin**, ETH Zurich

Title: *Cryptographically Sound Protocol-Model Abstractions*

We present a formal theory for cryptographically-sound theorem proving. Our starting point is the Backes-Pfitzmann-Waidner (BPW) model, which is a symbolic protocol model that is cryptographically sound in the sense of blackbox reactive simulatability/UC. To achieve cryptographic soundness, this model is substantially more complex than standard symbolic models and the main challenge in formalizing and using this model is overcoming this complexity. We present a series of models that successively abstract the original BPW model, bringing it closer to standard Dolev-Yao style models, while preserving cryptographic soundness. As our models are state-based, we have also developed monad-based tools for formalizing and reasoning about these models. We present a case study showing that our abstractions and tools enable proofs of complexity comparable to those based on more standard models. Our entire development has been formalized in Isabelle/HOL.

**Martin Grohe**, Humboldt University Berlin

Title: *The Quest for a Logic Capturing PTIME*

The question of whether there is a logic that captures polynomial time
is the central open problem in descriptive complexity theory. It was
first asked by Chandra and Harel (1982) in the context of database
theory, and later in a slightly different form by Gurevich (1988) in
the context of finite model theory. Essentially, a logic captures
PTIME if the properties of finite structures definable in the logic
are precisely those decidable in polynomial time. (But there are
subtleties in the definition of what constitutes a logic in this
context.)

In this talk, I will review the question and the early, mostly
negative results that were obtained until the mid 1990s. I will then
turn to positive results showing that fixed-point logic with counting
captures PTIME on several interesting classes of structures, among
them planar graphs and graphs of bounded tree width. This part of the
talk will include recent results on definability in fixed-point logic
and graph structure theory. Finally, I will dicuss stronger logics
formed by adding algebraic operators to fixed-point logic, and I will
propose some open problems and directions for further research.

**Dexter Kozen**, Cornell University

Title: *Nonlocal Flow of Control and Kleene Algebra with Tests*

Kleene algebra with tests (KAT) is an equational system for program verification that combines Kleene algebra (KA), or the algebra of regular expressions, with Boolean algebra. It can model basic programming and verification constructs such as conditional tests, while loops, and Hoare triples, thus providing a relatively simple equational approach to program equivalence and partial correctness. In this paper we show how KAT can be used to give a rigorous equational treatment of control constructs involving nonlocal transfer of control such as gotos, loop statements with multi-level breaks, and exception handlers. We develop a compositional semantics and an equational axiomatization. The approach has some novel technical features, including a treatment of multi-level break statements that is reminiscent of de Bruijn indices in the variable-free lambda calculus. We illustrate the use of the system by giving a purely calculational proof that every deterministic flowchart program is equivalent to a loop program with multi-level breaks.

**Yiannis Moschovakis**, UCLA and University of Athens

Title: *The Axiomatic Derivation of Absolute Lower Bounds*

The ancient Euclidean algorithm computes the greatest common divisor
gcd(m,n) of two natural numbers from (or relative to) the remainder
operation, rem, which is assumed as primitive; it requires no more
than 2 log(min(m,n)) applications of the remainder operation to
compute gcd(m,n) (for m,n >= 2), and it is not known to be optimal:

Conjecture. For every algorithm A which computes on N from
rem the greatest common divisor function, there is a
constant r>0 such that for infinitely many pairs a>=b>=1,
c_A(a,b) >= r log_2(a),

where c_A(m,n) counts the number of calls to ``the remainder
oracle'' required by α for the computation of gcd(m,n). The conjecture
claims a logarithmic lower bound for all algorithms which compute
gcd(m,n) from the remainder operation, not just those expressed by a
specific class of computation models.

In this lecture I will develop an approach to the theory of algorithms
in the style of abstract model theory which makes it possible to make
precise and (on occasion) prove the existence of non-trivial, absolute
lower bounds for a wide variety of problems and specified primitives.

Back to the LICS 2008 web page.

Last modified: Mon Mar 31 20:34:13 CEST 2008

Stephan Kreutzer and Nicole Schweikardt

Stephan Kreutzer and Nicole Schweikardt