Detail

Distributed temporal logic for security protocol analysis

We introduce a version of distributed temporal logic for rigorously
formalizing and proving metalevel properties of different security protocol models, and
establishing relationships between models. The resulting logic is quite expressive
and provides a natural, intuitive language for formalizing both local (agent specific) and
global properties of distributed communicating processes. Through a sequence of examples,
we show how this logic may be applied to formalize and establish the correctness
of different modeling and simplification techniques, which play a role in
building effective protocol tools.

Joint work with David Basin and Luca Viganò.