Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Electronic Notes in Theoretical Computer Science

Classical Knowledge for Quantum Security

Ellie D’Hondt, Mehrnoosh Sadrzadeh

Published Feb 1, 2011• 2 citations
Publisher

Abstract

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.
DOI
10.1016/j.entcs.2011.01.014

Related papers

Classical Knowledge for Quantum Security

Ellie D’Hondt, Mehrnoosh Sadrzadeh

We propose a decision procedure for analysing security of quantum cryptographic protocols, combining a classical algebraic rewrite system for knowledge with an operational semantics for quantum distributed computing. As a test case, we use our procedure to reason about security properties of a recently developed quantum secret sharing protocol that uses graph states. We analyze three different scenarios based on the safety assumptions of the classical and quantum channels and discover the path of an attack in the presence of an adversary. The epistemic analysis that leads to this and similar types of attacks is purely based on our classical notion of knowledge.

•Aug 26, 2008•1 citation

Classical knowledge for quantum security (extended abstract)

Ellie D’Hondt, Mehrnoosh Sadrzadeh

We propose a decision procedure for analysing security of quantum cryptographic protocols, combining a classical algebraic rewrite system for knowledge with an operational semantics for quantum distributed computing. As a test case, we use our procedure to reason about security properties of a recently developed quantum secret sharing protocol that uses graph states. We analyze three different scenarios based on the safety assumptions of the classical and quantum channels and discover the path of an attack in the presence of an adversary. The epistemic analysis that leads to this and similar types of attacks is purely based on our classical notion of knowledge.

•Jan 1, 2008•0 citations

Classical Knowledge for Quantum Security

D'Hondt, Ellie, Mehrnoosh Sadrzadeh

We propose a decision procedure for analysing security of quantum cryptographic protocols, combining a classical algebraic rewrite system for knowledge with an operational semantics for quantum distributed computing. As a test case, we use our procedure to reason about security properties of a recently developed quantum secret sharing protocol that uses graph states. We analyze three different scenarios based on the safety assumptions of the classical and quantum channels and discover the path of an attack in the presence of an adversary. The epistemic analysis that leads to this and similar types of attacks is purely based on our classical notion of knowledge.

arXiv:0808.3574•Aug 26, 2008•0 citations

Classical Knowledge for Quantum Cryptographic Reasoning

Vincent Danos A, Ellie D’Hondt

We prove that quantum key distribution is secure against several types of attacks within the framework of classical knowledge knowledge for quantum systems, a formal model which was developed in [D'Hondt, E. and P. Panangaden, Reasoning about quantum knowledge, in: Proceedings of the 25th Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS 3821, 2005, p. 0544c (to appear), quant-ph/0507176]. In particular we rephrase security as a logical property and use meta-logic reasoning on the finite state machine corresponding to the quantum key distribution protocol. While these security issues have been studied before, it is the logical-based approach that is original here.

Electronic Notes in Theoretical Computer Science•Nov 1, 2008•3 citations

An Epistemic Measurement System for Quantum Security

Elham Kashefi, Mehrnoosh Sadrzadeh

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

•Jan 1, 2007•0 citations

Knowledge in quantum systems (Extended Abstract

Ron van der Meyden, Manas Patra

This paper applies to quantum systems a modelling for the logic of knowledge, originally developed for reasoning about distributed systems, but since then applied to game theory, computer security and artificial intelligence. A formal model of quantum message passing systems is developed and the question of how one might define the semantics of a modal operator for knowledge in this model is considered. It is argued that there are at least two plausible semantics, depending on whether the agents are permitted to make use of their quantum state in determining what they know, and on whether one is dealing with single instances of quantum systems, or ensembles. The framework is illustrated using a number of examples from the quantum computing literature, including protocols for quantum key distribution and teleportation. 1

•Jan 1, 2003•2 citations
We propose a decision procedure for analysing security of quantum cryptographic protocols, combining a classical algebraic rewrite system for knowledge with an operational semantics for quantum distributed computing. As a test case, we use our procedure to reason about security properties of a recently developed quantum secret sharing protocol that uses graph states. We analyze three different scenarios based on the safety assumptions of the classical and quantum channels and discover the path of an attack in the presence of an adversary. The epistemic analysis that leads to this and similar types of attacks is purely based on our classical notion of knowledge.
We propose a decision procedure for analysing security of quantum cryptographic protocols, combining a classical algebraic rewrite system for knowledge with an operational semantics for quantum distributed computing. As a test case, we use our procedure to reason about security properties of a recently developed quantum secret sharing protocol that uses graph states. We analyze three different scenarios based on the safety assumptions of the classical and quantum channels and discover the path of an attack in the presence of an adversary. The epistemic analysis that leads to this and similar types of attacks is purely based on our classical notion of knowledge.
We propose a decision procedure for analysing security of quantum cryptographic protocols, combining a classical algebraic rewrite system for knowledge with an operational semantics for quantum distributed computing. As a test case, we use our procedure to reason about security properties of a recently developed quantum secret sharing protocol that uses graph states. We analyze three different scenarios based on the safety assumptions of the classical and quantum channels and discover the path of an attack in the presence of an adversary. The epistemic analysis that leads to this and similar types of attacks is purely based on our classical notion of knowledge.
We prove that quantum key distribution is secure against several types of attacks within the framework of classical knowledge knowledge for quantum systems, a formal model which was developed in [D'Hondt, E. and P. Panangaden, Reasoning about quantum knowledge, in: Proceedings of the 25th Conference on Foundations of Software Technology and Theoretical Computer Science, LNCS 3821, 2005, p. 0544c (to appear), quant-ph/0507176]. In particular we rephrase security as a logical property and use meta-logic reasoning on the finite state machine corresponding to the quantum key distribution protocol. While these security issues have been studied before, it is the logical-based approach that is original here.
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
This paper applies to quantum systems a modelling for the logic of knowledge, originally developed for reasoning about distributed systems, but since then applied to game theory, computer security and artificial intelligence. A formal model of quantum message passing systems is developed and the question of how one might define the semantics of a modal operator for knowledge in this model is considered. It is argued that there are at least two plausible semantics, depending on whether the agents are permitted to make use of their quantum state in determining what they know, and on whether one is dealing with single instances of quantum systems, or ensembles. The framework is illustrated using a number of examples from the quantum computing literature, including protocols for quantum key distribution and teleportation. 1