An Epistemic Measurement System for Quantum Security

We develop a formal system to reason about knowledge properties of quantum security protocols. The formalism is obtained via a marriage of measurement calculus [3], an algebraic framework for measurementbased quantum computing [7], with the algebra of epistemic actions and their appearance maps [1, 8]. Measurement calculus has also proven to be a proper language to describe and to analyse distributed quantum protocols [4]. Protocols (here referred to as measurement pattern) are described by a combination of commands: 1-qubit preparations Ni (prepares qubit i in state |+〉i), 2-qubit entanglement operators Eij: = ∧Zij (controlled-Z operator), 1-qubit measurements M α i, and 1-qubit Pauli corrections Xi and Zi, where i, j represent the qubits on which each of these operations apply, and α ∈ [0, 2π). Measurement M α i is defined by orthogonal projections P |+α〉 i (with outcome si = 0) and P |−α〉 i (with outcome si = 1). 1 Dependent corrections, used to control non-determinism, will be written X sj i and Zsj i, with X0 i = Z0 i = I, X1 i = Xi, and Z1 i = Zi. Any pattern can be put in a standard form, where all the preparation and entanglement