First-order logic formalization for security protocols and attackers enables formal verification. Once a formalization is established, standard tools such as a theorem prover can be used in the analysis.

Central to the formalization presented by the authors is a predicate for indistinguishability, that is, terms cannot be distinguished by a polynomial-time Turing machine with non-negligible probability. With the help of such a predicate, cryptographic properties such as the decisional Diffie-Hellman assumption can be axiomatized. The axioms are later translated into the language of the Coq theorem prover.

The authors build on their own previous work in first-order formalization, tackling multiple sessions in a protocol. To this end, they present and axiomatize an if_then_else statement.

The ideas are presented in detail and illustrated using the Diffie-Hellman key exchange. Because they focus the paper on extending their own previous work, the authors address readers from their particular field. The paper is not an ideal starting pointing for novices due to its heavy use of acronyms from the security field and many references to previous work.