Classical Knowledge for Quantum Security

We propose a decision procedure for analysing security of quantum cryptographic protocols, combining an algebraic logic rewrite system with an operational semantics for quantum distributed computations. We apply our approach to reasoning about security properties of a recently developed quantum secret sharing protocol.