DRAFT

Linear epistemic logic can be used to reason about changing knowledge states of agents acting in a system. Here we use it to formalize the Needham-Schröder-Lowe public-key authentication protocol for establishing secure communication sessions. We have developed a notion of adequacy to refer to the formal compositional corre-spondence between the protocol and the formalism. Through the iterative process of attempting to prove adequacy theorems and noting where and how the proof breaks down, we have been able to refine the formalism so that it adheres to the structure and semantics of the protocol as it was originally specified. This work is the first step towards showing that rigorous formal reasoning can be applied to protocols and processes followed in the wild