PUBLIC VIVA-VOCE NOTIFICATION
2.00 pm, Seminar Hall
A theory of assertions for Dolev-Yao models
Vaishnavi Sundararajan
Chennai Mathematical Institute.
29-08-18

---

Abstract

In the last couple of decades, much attention has been paid to modeling and analyzing security protocols with a view to formal verification. A popular formal model is one known as the Dolev-Yao model, which was proposed in 1983. Many enhancements to the basic Dolev-Yao model have been proposed over the years to capture more complicated features of real-life protocols. In this talk, we study one such extension, concerning certification in protocols.

We undertake an abstract study of certification in security protocols, concentrating on the logical properties and derivability of certificates. Specifically, we extend the Dolev-Yao model with a new class of objects called ‘assertions’ which represent certificates, along with an associated algebra for deriving new assertions from old ones. Assertions have a simple syntax, with equality, conjunction, disjunction and existential quantification. The presence of the quantifier makes the derivability problem an interesting challenge, and we provide algorithms and complexity bounds for this problem as well as the active intruder problem for this model.