论文标题
PFMC：安全协议验证的并行符号模型检查器
PFMC: a parallel symbolic model checker for security protocol verification
论文作者
论文摘要
我们对平行模型检查器的设计和实施进行了调查，以进行安全协议验证，该验证基于对手的符号模型，在该模型中，避免了具体术语和消息的实例化，直到需要解决特定主张为止。我们建议以这种自然懒惰的方法来平行这种象征性状态探索和评估。我们利用Haskell中的策略概念，该策略从线程管理的低水平细节中抽象出来，并模块化添加了并行评估策略（在Haskell中封装为单调）。我们以现有的符号模型检查器OFMC为基础，该模型已在Haskell中实现。我们表明，对于Dolev-Yao Attacker模型和更一般的代数攻击者模型，从原始的单线程实现到我们的多线程版本时，速度的提高速度非常明显约3-5倍。我们确定了与模型检查器并行的几个问题：除其他外，控制记忆消耗的增长，平衡懒惰与严格的评估以及实现并行性的最佳粒度。
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.
