PFMC: a parallel symbolic model checker for security protocol verification

TL;DR

This paper introduces PFMC, a parallel symbolic model checker for security protocols that significantly speeds up verification by leveraging Haskell's parallel strategies, addressing challenges like memory management and evaluation balancing.

Contribution

It presents a novel parallel implementation of a symbolic model checker for security protocols using Haskell's strategies, achieving substantial performance improvements.

Findings

3-5 times speedup over single-threaded version

Effective parallelisation of symbolic state exploration

Identified key issues in parallel model checking such as memory growth and evaluation balance

Abstract

We present an investigation into the design and implementation of a parallel model checker for security protocol verification that is based on a symbolic model of the adversary, where instantiations of concrete terms and messages are avoided until needed to resolve a particular assertion. We propose to build on this naturally lazy approach to parallelise this symbolic state exploration and evaluation. We utilise the concept of strategies in Haskell, which abstracts away from the low-level details of thread management and modularly adds parallel evaluation strategies (encapsulated as a monad in Haskell). We build on an existing symbolic model checker, OFMC, which is already implemented in Haskell. We show that there is a very significant speed up of around 3-5 times improvement when moving from the original single-threaded implementation of OFMC to our multi-threaded version, for both the Dolev-Yao attacker model and more general algebraic attacker models. We identify several issues in parallelising the model checker: among others, controlling growth of memory consumption, balancing lazy vs strict evaluation, and achieving an optimal granularity of parallelism.