Verification of Stateful Protocols
There are at least three reasons why it is desirable to perform proofs of security in a proof assistant like Isabelle/HOL or Rocq. First, it gives us an overwhelming assurance that the proof of security is actually a proof and not just the result of a bug in a complex verification tool.
This is because the basic idea of an LCF-style theorem prover is to have an abstract datatype theorem so that new theorems can only be constructed through functions that correspond to accepted proof rules; thus implementing just this datatype correctly prevents us from ever accepting a wrong proof as a theorem, no matter what complex machinery we build for automatically finding proofs. Second, a human may have an insight of how to easily prove a particular statement where a “stupid” verification algorithm may run into a complex check or even be infeasible. Third, the language of a proof assistant can formalize all accepted mathematics, so there is no narrow limit on what aspects of a system we can formalize. For instance, we have proved in Isabelle/HOL a compositionality result for our protocol model: given a set of protocols for which we have proved security and that meet a number of requirements, then also their composition is correct. Since also the said requirements are proved in Isabelle, we arrive at a full security proof of the entire system checked by Isabelle. A result like this is beyond the scope of any standard verification tool. Note also that as part of the composition, some of the component protocols may be proved secure by different methods or even automatically.
With our work, we aim for achieving the high assurance of an LCF-style theorem prover (namely, Isabelle/HOL) with a highly-automated verification approach for a well-defined fragment of stateful (security) protocols. The result is both an extensive formalization of stateful protocols and a fully-automated verification method, i.e., a tool. In more detail, our work has two contributions:
- The formalization in Isabelle of the abstract interpretation approach for stateful protocols as the PSPSP tool. In a nutshell, we have implemented in Isabelle the computation of the abstract fixed point—the proof idea so to speak—and how Isabelle can convince herself that this fixed point covers everything that can happen in the concrete protocol. The Isabelle security proof that one obtains consists of two main parts: first, we have a number of protocol-independent theorems that we have proved in Isabelle once and for all, and second, for every protocol and fixed point, we have a number of checks that Isabelle can directly execute to establish the correctness of the given protocol. The entire protocol-independent formalization consists of more than 25,000 lines of Isabelle code (definitions, theorems and proofs).
- The development and integration into Isabelle of a simple protocol specification language for stateful protocols that is based on a notion of atomic transactions: in a transaction, an entity may receive a message, consult its long-term database, make changes to the database and finally send out a reply. This language is more high-level than for instance multi-set rewriting while directly defining a state-transition system. The language additionally allows the specification of analysis rules which are rules that express how the intruder can extract knowledge from received messages built using cryptographic functions.
The full details are described in our latest paper [1] that just has been accapted in the Journal of Computer Security. The formalization in Isabelle/HOL, including the tool PSPSP (implemented in Isabelle/HOL), is available in the Archive of Formal Proofs (AFP) [2].