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 of Danos- Kashefi-Panangaden, which is an algebraic framework for measurement-based quantum computing of Briegel-Browne-Raussendorf, with the algebra of epistemic actions developed in the work of Baltag-Coecke-Sadrzadeh. Our setting consists of a quantale of deterministic well-defined measurement calculus patterns and a right module of results of measurement, both endowed with appearance maps standing for information of agents involved in the actions. As an example we encode and reason about the authentication and secrecy properties of Ekert'91 protocol and its corresponding attack.