A Testing Theory for a Higher-Order Cryptographic Language

Abstract

We study a higher-order concurrent language with cryptographic primitives, for which we develop a sound and complete, first-order testing theory for the preservation of safety properties. Our theory is based on co-inductive set simulations over transitions in a first-order Labelled Transition System. This keeps track of the knowledge of the observer, and treats transmitted higher-order values in a symbolic manner, thus obviating the quantification over functional contexts. Our characterisation provides an attractive proof technique, and we illustrate its usefulness in proofs of equivalence, including cases where bisimulation theory does not apply.