ABSTRACT
Starting from a historical example, namely the Needham-Schroeder public key protocol, this chapter discusses the modeling of cryptographic protocols as infinite state machines to achieve the highest possible confidence in their actual enforcement of expected security properties. Accordingly, the verification of such properties demands the construction of mathematical proofs, based on generalized mathematical induction, in a logical calculus. The number and the subtlety of the cases arising in those proofs, along with the required logical calculus expressiveness, render interactive theorem provers, such as Isabelle/HOL, the only viable option. The chapter illustrates two methods allowing for formal protocol verification according to the approach, both based on Isabelle/HOL, namely Paulson's inductive method and the author's own relational method, by considering their application to the Needham-Schroeder-Lowe protocol and to a sample PAKE protocol, respectively, and detailing how they enable to model relevant real-world entities (agents, messages, attacker's capabilities, protocol rules and properties).
