Abstract Sequential Programs and a Logic of Events
         Mark Bickford  (ATC-NY and Cornell University)

Requirements for distributed systems can be expressed naturally in terms of
events. Within a logical theory of events, these requirements can be refined
to a collection of constraints that imply the original requirements.
Requirements and refinements can be expressed very abstractly in terms of
"event classes" that associate values with selected events. An event class
is a partial function on a "spacetime" of causally-ordered events; it is
analogous to the concept of a "field" in physics. When the values of events
in a class depend on only local information, then the class is
"programmable" and a further refinement can introduce explicit state
variables and a program that implements the class. We will illustrate these
concepts and methods with simple examples.

The correctness of some algorithms depend on the fact that the certain
events occur in a particular sequence. The events bound by such sequential
contraints form "threads" or "chords" and a single agent may simultaneously
engage in multiple chords. Process calculi and dynamic logic are some of the
methods that have been used to reason about such sets of sequential
programs. We show how such reasoning can also done in the logic of events by
expressing the constraints on sequential threads using a simple scheme for
"lawful behavior".

We will illustrate these ideas with a simple example of a challenge-response
authentication protocol.
This example will also show how we can abstractly express and reason about
"nonces" and digital signatures using
event classes whose values include "atoms".

Our concepts are abstract enough to apply to any event-based semantics, and
the examples should provide the basis for comparison with related structures
such as Strand spaces or Protocol Composition Logic (PCL) that are used in
the analysis of security properties. The methods for expressing programs
abstractly in terms of constraints on event classes can be used for
reasoning about any properties of distributed programs. Time permitting, we
will discuss a formalization and proof of Lamport's "Bakery Algorithm" for
mutual exclusion in terms of events.