Seminário Segurança de Informação 

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.