The formal analysis of cryptographic protocols traditionally focuses on trace and equivalence properties, for which decision procedures in the symbolic (or Dolev-Yao, or DY) model are known. However, many relevant security properties are expressed as DY hyperproperties that involve quantifications over both execution paths and attacker computations (which are constrained by the attacker’s knowledge in the underlying model of computation). DY hyperproperties generalise hyperproperties, for which many decision procedures exist, to the setting of DY models. Unfortunately, the subtle interactions between both forms of quantifications has been an obstacle for lifting decision procedures from hyperproperties to DY hyperproperties.

The central contribution of the paper is the first procedure for deciding DY hyperproperties, in the usual setting where the number of protocol sessions is bounded and where the the equational theory modelling cryptography is subterm-convergent. The main technical innovation of our procedure is the notion of proof stack, which controls the interactions between attacker computations and path quantifications. We prove that our decision procedure can decide the validity of any hyperproperty in which quantifications over messages are guarded and quantifications over attacker computations is limited to expressing attacker’s knowledge. We also establish the complexity of the decision problem for several important fragments of the hyperlogic. We illustrate the techniques and scope of our procedure through examples of smart contracts.