  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.
