26/10/2007, 16:00 — 17:00 — Tagus-1.1
Jan Cederquist, Instituto Superior Técnico
Verifying Liveness in Security Protocols
We will discuss automatic verification of liveness properties in
security protocols. Liveness properties only hold in general in the
Dolev-Yao intruder model if at least some communication channels
are resilient. However, the complexity of the resilient
communication channels assumption, when used as a fairness
constraint, indicates that the Dolev-Yao model is not suitable for
automatic verification of liveness properties. Here we present a
modified Dolev-Yao intruder that is more suitable for verifying
liveness properties. As an application, formal verification of fair
exchange protocols is discussed.
Notice the change of schedule!