Mind the Gap Connecting Protocol Representations in Squirrel

Abstract

Security protocols are concurrent processes that communicate using cryptography to achieve various security properties. Their formal verification has been the subject of much research, which has led to a number of successful tools. Several of these tools use variants of the applied pi-calculus as an input language to model protocols, though the internal representation used for verification may vary. The translation from processes to their internal representation has received relatively little attention despite its important role in the soundness and efficiency of the security analyses. We consider this problem within the Squirrel prover framework, where processes are translated to so-called systems of actions, which serve as the basis for a logic-based verification technique. Intuitively, actions consist of groups of elementary instructions. We provide a general theory for grouping instructions in a way that preserves both indistinguishability and trace properties, and we instantiate it to obtain a new translation procedure for Squirrel. We have implemented our procedure as a replacement of the original (unsound) translation, demonstrating that it can serve as an almost drop-in replacement in existing case studies.