* $\sigma$ samples a random stabilizer $x \sample \{0,1\}^n$, applies $\gateX^{x_{M'}}\gateZ^{(G_M' x)_{M'}}$ where $M' \eqdef \{i \mid c_i = 1\}$ on the received $\ket{G}_M$ and sends the resulting qubits of parties in $M'$ to the distinguisher.

* Then, $\sigma$ receives a set of corrections $(a_i, b_i) \in (\{0,1\}^{|H|})^2$ for $i \in M'$, computes $x'_H \eqdef \xor_i a_i$  and $z'_H \eqdef \xor_i b_i$, and checks that $f_G(M', x'_H, z'_H) = \top$ (otherwise it sends $c_i' = \bot$ to $\Verif$ for all $i$ and aborts).

* Since $f_G(M', x'_H, z'_H) = \top$, let $b$ be like in <ref>, and let us define $x'_M \eqdef (V^T)^{-1}
\begin{bmatrix}
\mathbf{0}
\end{bmatrix}
$, and $x' \eqdef
\begin{bmatrix}
\end{bmatrix}

* If the set of corrupted parties contains no party in $[n]$, the simulator can stop. Otherwise, it will receive bits $c_i''$ (sent to $\CoinFlip$ in the real world and called $c_i$ there). It will then send $x \xor x'$ to parties that sent $c_i'' = \bot$, wait for a bit from each party (sent to $\CoinFlip$ in the real world and denoted $c_i'$), and abort if one of these party sent $\bot$, by sending $c_i' = \bot$ to the ideal functionality for all $i \in M$. Finally, it broadcasts $x$ to all parties such that $c_i = 1$.

* For each party $i$ such that $c_i = 0$, $\sigma$ will apply on the $i$-th qubit (that remains from the second step) the operation $\gateX^{x_i \xor x_i'}\gateZ^{(G (x \xor x'))_i}$, and output the resulting qubit to the distinguisher.

* Finally, it outputs $c_i' = \top$ to $\Verif$ in order to let the functionality broadcast $\ket{G}_{\bar{M}}$ to all honest parties.

By construction, this simulator follows exactly the abort pattern of the real world protocol, and the exchanged messages are identical. So without loss of generality, we can assume that the distinguisher never aborts[We can always turn a distinguisher that aborts into a distinguisher that does not abort while increasing the probability of distinguishing, for instance by intercepting all abort messages from the original distinguisher, and continuing instead the protocol with arbitrary non-aborting inputs while sending to the original distinguisher the messages that would have been sent in both the ideal and the real protocol.], and in particular sends valid corrections. Similarly, we can assume that the distinguisher is always sending $c_i = 1$ since the case $c_i = 0$ can easily be simulated by the distinguisher given the transcript for $c_i = 1$ since it contains more information. Under this assumption, both the real and ideal worlds can significantly be simplified:

* In the real world, the distinguisher receives first $\ket{G}_M$, then send some (valid) corrections defining $x'_H = \xor_i a_i$ and $z'_H \eqdef \xor_i b_i$, and finally receives the remaining qubits $\gateX^{x_H \xor x_H'} \gateZ^{z'_H \xor (G x)_H}\ket{G}_H$ together with $x$ that was sampled uniformly at random.

* In the ideal world, the distinguisher receives first $\gateX^{x_M}\gateZ^{(G x)_M}\ket{G}_M$ where $x$ is sampled uniformly at random, then it sends some (valid) corrections defining $x'_H = \xor_i a_i$ and $z'_H \eqdef \xor_i b_i$, and finally receives the remaining qubits $\ket{G}_H$ together with $x \xor x'$ where $x'_M \eqdef (V^T)^{-1}
\begin{bmatrix}
\mathbf{0}
\end{bmatrix}
$, and $x' \eqdef
\begin{bmatrix}
\end{bmatrix}

First, we can realize that since $\gateX^{x_M}\gateZ^{(G x)_M}\ket{G} = \gateX^{x_M}\gateZ^{(G x)_M}(\gateX^{x }\gateZ^{G x} \ket{G}) = \gateX^{x_H}\gateZ^{(G x)_H}\ket{G}$, the ideal world is indistinguishable from a world where the distinguisher receives $\ket{G}_M$ while the functionality applies $\gateX^{x_H}\gateZ^{(G x)_H}$ on the remaining qubits. This gives this equivalent hybrid system:

* The distinguisher receives first $\ket{G}_M$ then it sends some (valid) corrections, defining $x'_H = \xor_i a_i$ and $z'_H \eqdef \xor_i b_i$, and finally receives the remaining qubits $\gateX^{x_H}\gateZ^{(G x)_H}\ket{G}_H$ (where $x$ is sampled uniformly at random) together with $x \xor x'$ where $x'_M \eqdef (V^T)^{-1}
\begin{bmatrix}
\mathbf{0}
\end{bmatrix}
$, and $x' \eqdef
\begin{bmatrix}
\end{bmatrix}

Then, we can define $\hat{x} \eqdef x \xor x'$. Since $x$ is independent of $x'$, the probability of sampling any $\hat{x}$ is equal to the probability of sampling any $x$, we can therefore sample $x'$ instead of $x$, and use the fact that $x = \hat{x} \xor x'$. So, the above system can be turned into the following indistinguishable system:

* The distinguisher receives first $\ket{G}_M$ then it sends some (valid) corrections defining $x'_H = \xor_i a_i$ and $z'_H \eqdef \xor_i b_i$, and finally receives the remaining qubits $\gateX^{\hat{x}_H \xor x'_H}\gateZ^{(G (\hat{x} \xor x'))_H}\ket{G}_H$ (where $\hat{x}$ is sampled uniformly at random) together with $\hat{x}$ where $x'_M \eqdef (V^T)^{-1}
\begin{bmatrix}
\mathbf{0}
\end{bmatrix}
$, and $x' \eqdef
\begin{bmatrix}
\end{bmatrix}

Finally, we have:

\begin{align}
(G x')_H
&= \begin{bmatrix}
G_H & \Gamma^T
\end{bmatrix} x' =
G_H x'_H \xor U^T
\begin{bmatrix}
I_r & 0\\
R^T & 0
\end{bmatrix}V^T x'_M
= G_H x'_H \xor \left(U^T
\begin{bmatrix}
I_r & 0\\
R^T & 0
\end{bmatrix}V^T\right)\left((V^T)^{-1}
\begin{bmatrix}
\mathbf{0}
\end{bmatrix}\right) \\
G_H x'_H \xor
U^T \begin{bmatrix}
R^T b
\end{bmatrix}
\eqeqDef{thm:mainThm}
G_H x'_H \xor
U^T (U^T)^{-1} (z'_H \xor G_H x'_H) =
\end{align}

Therefore, we get $\gateX^{\hat{x}_H \xor x'_H}\gateZ^{(G (\hat{x} \xor x'))_H}\ket{G}_H = \gateX^{\hat{x}_H \xor x'_H}\gateZ^{z'_H \xor (G \hat{x})_H}\ket{G}_H$. Hence, this last system is actually equal to the real world, which concludes the indistinguishability proof.

[][end, restate]
Assuming the existence of a protocol for graph state verification fulfilling properties described in <ref> and a coin flipping protocol realizing , there exists a protocol realizing $\Verif$.

This is a direct consequence of <ref> and <ref>, where we run in <ref> the graph state verification instead of $\Verif^f$ and the coin flipping protocol instead of .

More precisely, in <ref>, we first proved the equivalence $\pi_{[n] \cup \source} \cR \approx \filter_{[n] \cup \source} \Verif^f$ between a concrete verification protocol and an ideal, but gruesome, resource. Then, in <ref>, we explicited the protocol $\{\tau_i\}_{i \in [n]}$, that applies a random stabilizer to the output state of the verification protocol, to construct a simpler functionality $\Verif$ from this gruesome resource alongside with a coin flipping resource. In particular, we proved the equivalence $ \bot_{[n] \cup \source} \Verif{}\approx \tau_{[n]} \filter_{[n]} (\Verif^f \| \CoinFlip) \filter_{\source} $.

Let $\pi'_{[n]}$ be a concrete protocol securely realising the ideal functionality $\CoinFlip$ using resource $\cR'$. We have, in particular, that $\pi'_{[n]}\cR' \approx \bot_{[n]}\CoinFlip$. By composability of resources within the AC framework, we get the correctness equivalence :

\begin{equation}
\pi_{[n] \cup \source}\circ\tau_{[n]}  (\cR \| \pi'_{[n]}\cR') \approx \bot_{[n] \cup \source} \Verif{} . \end{equation}

For all subset of malicious parties $M$, we can similarly appropriately compose the simulators from the proofs of the secure construction of $\CoinFlip$, $\Verif^f$ and $\Verif$ to obtain simulators $\sigma_M$. We can use these simulators and the composability of AC to similarly prove all the equivalences necessary in the Security <ref>. This proves the secure construction of the ideal functionality $\Verif$ by a graph state verification protocol fulfilling properties described in <ref> and a coin flipping protocol realizing .

§ USE CASES

§.§ Proofs of <ref>

Our result readily applies to some already existing protocols in the literature. In the following we show two such use cases and discuss their implication and improvement over previous works.

§.§ Generic translation tools

Before studying specific protocols, it is handy to first derive some generic theorems in order to translate between the notations used in existing graph state verification protocols and the notion of distance used in <ref>. Indeed, while our notion of distance uses a single parameter $\eps$ quantifying the average distance to the ideal graph state (which is handy since in AC we have a single parameter $\eps'$ used to denote the distance between two systems $A \approx_{\eps'} A$), existing works consider instead two parameters, namely the probability $\delta$ of being $\eta$-close to the ideal graph state.

We also emphasize that most existing protocols implicitly assume that either all parties abort or that they all accept the final state together. We will refer to that property as simultaneous abortion. While <ref> does not strictly enforce this behavior, any protocol that does not fulfill simultaneous abortion with high probability will also have low guarantee in term of security. Said differently, the $\eps$ obtained in <ref> and <ref> will be far from $0$. This makes sense since our resource <ref> always sends the same abort/accept bit to all parties. So, if the adversary can send different abort bits to different parties, this gives directly a simple way to distinguish the ideal world from the real world, by simply checking if all parties share the same abort bit.

This could be a real issue in practice, for instance in <cit.> if a malicious verifier is picked, the verifier could send different abort bits to all parties. As a result, without further checks, this protocol could only be proven composably secure for some constant $\eps$ (as a reminder, in the original protocol, we expect to be able to get $\eps$ as small as wanted, the running time scaling polynomially with $O(1/\eps)$). We have two options to avoid this issue:

* Either change the definition of $\Verif$ to get rid of simultaneous abortion, meaning that some honest parties could abort while others would not.

* Or we could slightly adapt the protocol using a broadcast channel, i.e. a channel where all parties receive the same bit, in order to notify to all parties at the same time the final abort bit.

Since the first option makes the resource harder to use, we will opt for the second solution. This makes even more sense as in existing protocols, the protocol already needs to obtain a random string known to all parties, which often already implicitly requires a broadcast channel. One might also ask whether, reciprocally, a broadcast channel is needed to realize $\Verif$. It turns out that $\Verif^f$ can already be (ab)used to obtain a kind of broadcast channel: since all parties see the same abort bit, one could decide that “abort” means 0 and that “accept” means 1. Therefore, it should come at no surprise that a broadcast channel is needed to realize $\Verif$.

[][end, restate]
Let $\Pi = \{\pi_i\}_{i \in [n] \cup \source}$ be a protocol generating, when all parties are honest, a state $\ket{G}$ shared among all parties but the source. We assume that $\Pi$ has simultaneous abortion (<ref>), i.e. that for any adversary $\cA$, either all honest parties abort at the same time with some probability $1-p$ or accept and output the averaged state $\rho_\top$. Then, if any of the following conditions is fulfilled, this protocol is an $\eps$-graph state verification protocol according to <ref>:

* If $p(1-F(\rho_\top, \Tr_{[n]\setminus H}(\ketbra{G}{G}))) \leq \eps$. This denotes the fact that the probability of accepting and outputting a state far from $\ket{G}$ to the honest parties is small.

* Or if $F(\rho_\top, \Tr_{[n]\setminus H}(\ketbra{G}{G})) \geq 1 - \eps$. This corresponds to the protocol's property to create a state close to the desired state. Note that this condition is strictly stronger than the first one, since an adversary might be able to produce such a state with negligible probability. Yet, unconditionally secure protocols might prefer this formulation.

Since the protocol is correct by assumption, the first point of <ref> is trivially fulfilled. We focus now on proving that the protocol is secure according to <ref>. Since the protocol has simultaneous abortion, the first part of the security statement is trivially true, hence we just need to find $\sigma$ such that <ref> is true. Let $\rho \eqdef \Tr_{[n] \setminus H}(\pi_{H} \cR \cA)$ be the averaged state obtained at the end of the interaction with $\cA$. Then, since $\pi$ has simultaneous abortion, we know that there exists $p \eqdef \bra{\bot^{|H|}} \rho \ket{\bot^{|H|}}$ (actually this is the same $p$ as in the lemma) such that:

\begin{align}
\rho = (1-p)\ketbra*{\bot^{|H|}}{\bot^{|H|}} + p\rho_\top
\end{align}

where $\rho_\top$ is a normalized state orthogonal to $\ketbra*{\bot^{|H|}}{\bot^{|H|}}$, corresponding to the averaged state obtained when no party aborted.

Let us define

\begin{align}
\sigma \eqdef p\Tr_{[n]\setminus H}(\ketbra{G}{G}) + (1-p) \ketbra*{\bot^{|H|}}{\bot^{|H|}}
\end{align}

and find $\eps$ such that $F(\rho,\sigma) \geq 1-\eps$, or, equivalently, such that $1-F(\rho,\sigma) \leq \eps$. To compute this quantity, we can first use the strong concavity of fidelity (<cit.>) that states that $F(\sum_i p_i \rho_i ,\sum_i q_i \sigma_i) \geq \sum_i \sqrt{p_i q_i} F(\rho_i ,\sigma_i)$. Therefore, we have:

\begin{align}
&\leq 1-(1-p)F(\ketbra*{\bot^{|H|}}{\bot^{|H|}}, \ketbra*{\bot^{|H|}}{\bot^{|H|}}) - p F(\rho_\top, \Tr_{[n]\setminus H}(\ketbra{G}{G}))\\
& = p(1-F(\rho_\top, \Tr_{[n]\setminus H}(\ketbra{G}{G})))\label{eq:poneminusf}
\end{align}

where the last equality is a direct consequence of $F(\ketbra{\phi}{\phi},\ketbra{\phi}{\phi}) = 1$ when $\ket{\phi}$ is a pure state. If any of the first two assumptions of this lemma are fulfilled, we can directly inject it in <ref> to obtain <ref>. This shows that the protocol is an $\eps$-graph state verification protocol according to <ref> (for the second assumption, we upper bound $p$ by $1$).

[][end, restate]
If a protocol has simultaneous abortion (<ref>), and if the probability (on the randomness of $\cA$ and the whole protocol) to have no abort and a final state far from the target $\ket{G}$ is small, more formally:

\begin{align}
\pr[\ket{\psi_i} \gets \pi_H \cR \cA]{\Tr_{[n] \setminus H}\ket{\psi_i} \neq \ket{\bot^H} \land \sqrt{1-F^2(\Tr_{[n] \setminus H}\ketbra{\psi_i}{\psi_i}, \Tr_{[n] \setminus H}\ketbra{G}{G})} \geq \eta} \leq \delta\label{eq:assumptionVersionF}
\end{align}

or, equivalently,

\begin{align}
\pr[\ket{\psi_i} \gets \pi_H \cR \cA]{\Tr_{[n] \setminus H}\ket{\psi_i} \neq \ket{\bot^H} \land \min_U \TD((I^H \otimes U^M)\ket{\psi_i}, \ket{G}) \geq \eta} \leq \delta\label{eq:assumptionVersionMin}
\end{align}

then this protocol is an $(\delta + \eta^2)$-graph state verification protocol according to <ref>.

First, the fact that these two definitions are equivalent comes from the fact that for pure states, $\TD(\ket{\psi},\ket{\phi}) = \sqrt{1-|\braket{\psi}{\phi}|^2}$ (<cit.>), hence:

\begin{align}
\min_U \TD((I^H \otimes U^M)\ket{\psi_i}, \ket{G})
& = \min_U \sqrt{1-|\bra{G}(I^H \otimes U^M)\ket{\psi_i}|^2}\\
& = \sqrt{1-\max_U |\bra{G}(I^H \otimes U^M)\ket{\psi_i}|^2}\\
& = \sqrt{1-F^2(\Tr_{[n] \setminus H}\ketbra{\psi_i}{\psi_i}, \Tr_{[n] \setminus H}\ketbra{G}{G})}
\end{align}

where the last equality comes from Uhlmann's theorem (<cit.>), and additionally remarking that all purifications are equal up to a local unitary on the purified space. In the following, we will therefore only consider the assumption involving the fidelity.

We will now simplify the assumption <ref>, but first let us define some notations. First, it will be handy to denote, like in <ref>, $\rho_\top$ as the averaged normalized state obtained by honest parties assuming that the protocol has not aborted:

\begin{align}
\rho_\top \eqdef \esp*[\ket{\psi_i} \gets \pi_H \cR \cA\\ \Tr_{[n] \setminus H}\ket{\psi_i} \neq \ket{\bot^H}]{\Tr_{[n] \setminus H} \ketbra{\psi_i}{\psi_i}}
\end{align}

If we denote by $\{\ket{\psi_i}\}_i$ the set of all states producible by a $\pi_H \cR \cA$, and if $p_i$ represents the probability of outputting $\ket{\psi_i}$ assuming that it is not aborting ($\Tr_{[n] \setminus H}\ket{\psi_i} \neq \ket{\bot^H}$), we have therefore:

\begin{align}
\rho_\top = \Tr_{[n] \setminus H} \left(\sum_i p_i \ketbra{\psi_i}{\psi_i}\right) \label{def:rhotopassum}
\end{align}

To simplify further the notation we define for brevity:

\begin{align}
F_i & \eqdef F(\Tr_{[n] \setminus H}\ketbra{\psi_i}{\psi_i}, \Tr_{[n] \setminus H}\ketbra{G}{G})\label{eq:notationFi} \\
F   & \eqdef F(\Tr_{[n] \setminus H}\ketbra{\psi}{\psi}, \Tr_{[n] \setminus H}\ketbra{G}{G})
\end{align}

Using this notation, we can simplify the LHS of the assumption <ref> as:

\begin{align}
&\pr[\ket{\psi} \gets \pi_H \cR \cA]{\Tr_{[n] \setminus H}\ket{\psi} \neq \ket{\bot^H} \land \sqrt{1-F^2} \geq \eta}\\
&= \pr*[\ket{\psi} \gets \pi_H \cR \cA]{\Tr_{[n] \setminus H}\ket{\psi} \neq \ket{\bot^H}}
\pr*[\ket{\psi} \gets \pi_H \cR \cA\\\Tr_{[n] \setminus H}\ket{\psi} \neq \ket{\bot^H}]{\sqrt{1-F^2} \geq \eta}
\end{align}

By defining $p \eqdef \pr*[\ket{\psi} \gets \pi_H \cR \cA]{\Tr_{[n] \setminus H}\ket{\psi} \neq \ket{\bot^H}}$ as the probability of non aborting, this is equal to:

\begin{align}
p \pr*[\ket{\psi} \gets \pi_H \cR \cA\\\Tr_{[n] \setminus H}\ket{\psi} \neq \ket{\bot^H}]{\sqrt{1-F^2} \geq \eta}
\end{align}

Then, using the fact that the probability for $\ket{\psi}$ to be equal to $\ket{\psi_i}$ is $p_i$, we can simplify this as:

\begin{align}
p \pr*[\ket{\psi} \gets \pi_H \cR \cA\\\Tr_{[n] \setminus H}\ket{\psi} \neq \ket{\bot^H}]{\sqrt{1-F^2} \geq \eta}
= p \sum _p p_i \pr*[]{\sqrt{1-F_i^2} \geq \eta}
= p \sum_{p \mid \sqrt{1-F_i^2} \geq \eta} p_i
\end{align}

Therefore, assumption <ref> is equivalent to:

\begin{align}
p \sum_{i \mid \sqrt{1-F_i^2} \geq \eta} p_i \leq \delta \label{eq:boundCepssimpler}
\end{align}

Now, we can remark that using <ref>, it is enough to show that $p(1-F(\rho_\top, \Tr_{[n]\setminus H}(\ketbra{G}{G}))) \leq \eps$ to prove that the protocol is an $\eps$-graph state verification protocol. Since we aim to upper bound $p(1-F(\rho_\top, \Tr_{[n]\setminus H}(\ketbra{G}{G})))$, we can simplify this expression as follows:

\begin{align}
& p(1-F(\rho_\top, \Tr_{[n]\setminus H}(\ketbra{G}{G})))\\
& \eqeq{def:rhotopassum} p\left(1-F\left(\sum_i p_i \Tr_{[n] \setminus H} \ket{\psi_i}, \Tr_{[n]\setminus H}(\ketbra{G}{G})\right)\right)                          \\
& \ \leq p\left(1-\sum_i p_i F_i\right) \tag{Concavity of fidelity (\cite[Ex.~9.20]{NC10_QuantumComputationQuantum})} \\
& \ = p\sum_i p_i \left(1- F_i\right) \tag{$\sum_i p_i = 1$}\\
& \ = p\sum_{i \mid \sqrt{1-F_i^2} \geq \eta} p_i \left(1- F_i\right) \nonumber + p\sum_{i \mid \sqrt{1-F_i^2} < \eta} p_i \left(1- F_i\right) \tag{Split the sum} \\
& \ \leq \delta + p\sum_{i \mid \sqrt{1-F_i^2} < \eta} p_i \left(1- F_i\right) \tag{Fidelity is $\geq 0$ + \cref{eq:boundCepssimpler}}
\end{align}

Now, in the remaining terms, we assume $\sqrt{1-F_i^2} < \eta$, i.e. $1-F_i^2 < \eta^2$. But since $0 \leq F_i \leq 1$, we have $0 \leq F_i^2 < F_i$ and therefore $1-F_i \leq 1-F_i^2 < \eta^2$.
Therefore, after injecting this in the previous equation, we get:

\begin{align}
p(1-F(\rho_\top, \Tr_{[n]\setminus H}(\ketbra{G}{G})))
&\leq \delta + p\sum_{i \mid \sqrt{1-F_i^2} < \eta} p_i \eta^2\\
&\leq \delta + \eta^2\tag{Upper bound probabilities by $1$}
\end{align}

§.§ GHZ-state verification

In <cit.>, the authors develop and analyze an $n$-party verification protocol consisting only of classical communication and local quantum operations once the state is shared. One of the parties, called the Verifier, has a central role in the protocol: it sends instructions to all parties and broadcasts the output of the verification. We recall the protocol of <cit.> in <ref>. In the AC language, it uses quantum and classical authenticated secret channels, a broadcast channel and a Common Random String resource (CRS) as concrete resources to build an ideal GHZ-state sharing functionality. Note that it is important that the random string is sent by the CRS once all parties received the state from the source.

Multipartite entanglement verification protocol

* The source creates an $n$-qubit state locally equivalent to the GHZ state (up to local Hadamard and phase shift $\sqrt{Z}$ gate) and sends each qubit $i$ to party $i$.

* After receiving the state, the parties receive $r \sample \{0,1\}^S$ and $i \sample [n]$ from a CRS resource, where $S$ is a security parameter. Note that the source should not reveal $r$ and $i$ before the state is received by all parties.

* If $r=0\dots0$, the state received at step $1$ is outputted by each party and the protocol stops.

* Otherwise, if $r \neq 0\dots 0$, party $i$ is designed as the Verifier.

* The Verifier selects for each $i\in[n]$ a random input $x_{i}\in\{0,1\}$ such that $\sum_{i=1}^{n}x_{i}\equiv 0 \mod 2$ and sends it to the corresponding party via an authenticated private classical channel resource. The Verifier keeps one to themselves.

* If $x_{i}=0$, party $i$ performs a Z operation on their qubit. If $x_{i}=1$, party $i$ performs a Hadamard operation.

* Each party $i$ measures their qubit in the $\{\ket{0},\ket{1}\}$ basis and sends their outcome $y_{i}$ to the Verifier via the classical channel.

* The Verifier accepts and broadcasts $b_{out}\eqdef 0$ if and only if

\begin{equation*}
\sum_{i=1}^{n}y_{i}\equiv\frac{1}{2}\sum_{i=1}^{n}x_{i} \mod 2
\end{equation*}

Otherwise, the Verifier broadcasts $b_{out}=1$ and the protocol aborts.

* If the Verifier has not rejected, we restart from Step 1.

This protocol has been extensively studied and presents desirable properties: notably the probability of aborting increases when the state sent by the source is further away from the target state (locally equivalent to) $\ket{GHZ}$, and this probability can be made arbitrary small by increasing the number of rounds. More precisely, for one round, if $\rho$ denotes the state shared among the parties by the source, and if the verifier is honest, the probability of aborting is $\pr{b_{out} = 1} = \frac{\tau^2}{4}$ with:

\begin{equation}
\tau = \min_{U}\mbox{TD}(\ketbra{GHZ}{GHZ}, U\rho U^\dagger)
\end{equation}

where TD is the trace distance and $U$ is an operator acting only on the space of the dishonest parties. Since the verifier might not always be honest, we can repeat this protocol to increase the abort probability when the state is maliciously prepared. The verification protocol thus consists in rounds where the source shares a state to the parties, who then samples $r \sample \{0,1\}^S$ to decide if they verify the state or if they keep it. This process goes on until until either $r=0\dots0$ in step (3), in which case the parties output a quantum state, or if $b_{out}=1$ in step (8), in which case the parties abort. The fact that the parties decide to verify or keep the state after it is shared ensures that possible malicious parties do not adapt their behaviour to a particular round. In <cit.>, the authors prove that the probability that a state $\ket{\psi}$ is accepted after repeating the protocol until $r=0\cdots0$, and $\ket{\psi}$ is further than $\eps$ from the GHZ state is given by:

\begin{equation}
\pr{\ket{\psi} \textrm{accepted} \land \min _{U} \mbox{TD}(U\ket{\Psi},\ket{GHZ}) \geq \epsilon} =  2^{-S} \frac{4 n}{h \eps^2}
\end{equation}

where $U$ acts on the space of the dishonest parties, $n$ is the total number of parties and $h$ is the number of honest parties.

In later work <cit.>, an experimental realization of a loss-tolerant variant of this protocol has been implemented, hinting towards practicability of this protocol in real-life networks. Note that the result that we show in this section also applies to this variant.

A previous composable security study of this protocol <cit.> could not show the composable security of this protocol in the case of a coalition on malicious party and source and conjectured that it was impossible to prove in the AC framework. Our present work answers this conjecture by the negative. The key difference with the previous work lies in <ref>, which allows local simulators to communicate between each others via an additional communication channel resource. Equivalently, this allows to consider a single global simulator having access to all the corrupted interfaces of the ideal result, which is actually the choice made by the Universal Composability framework. Building on the work from the previous sections, we can show the following lemma proving composable security of the protocol from <cit.>:

[][end, restate]
The protocol defined in <cit.>, assuming that we use a broadcast channel to transmit the abort bit, is an $\eps$-graph state verification protocol for $\eps \eqdef \frac{1}{2^{S/2}}(4n + 1)$, where $2^S$ is the average number of tests before outputting a state as defined in <cit.> and $n$ is the total number of parties. As a result, it $(2\sqrt{2\eps - \eps^2})$-realizes $\Verif[\ket{G}]^f$ as defined in <ref>, and can be turned into a protocol that $(2\sqrt{2\eps - \eps^2})$-realizes $\Verif$.

This is a corollary of <ref>, using the second version of the assumption (<ref>). The probability in <ref> corresponds exactly to the $\pr{C_\eps}$ defined in <cit.> right before Theorem 3. This same theorem actually states that for any $\eps > 0$, $\pr{C_\eps} \leq \frac{4n}{2^{S} h \eps^2}$, where $2^S$ is the average number of tests before outputting a state as defined in <cit.>, $n$ is the total number of parties, and $h$ is the number of honest parties.

In AC the distance between two resources is the same irrespective of the number of corrupted parties. We thus aim to upper bound this by a number independent from the number of malicious parties. We can assume that at least one party is honest, i.e. $h \geq 1$, to get $\pr{C_\eps} \leq \frac{4n}{2^{S} \eps^2}$.  Since this is true for any $\eps$, we can in particular define:

\begin{align}
\eta &\eqdef \sqrt[4]{\frac{1}{2^S}} \label{def:epsstar}\\
\delta &\eqdef \frac{4n}{2^{S} \eta^2} = \frac{4n}{2^{S/2}}
\end{align}

and we have $\pr{C_\eta} \leq \delta$. So we can apply <ref> to show that the protocol is a $\delta + \eta^2$-graph state verification protocol, i.e. an $\eps$-graph state verification protocol for $\eps \eqdef \delta + \eta^2 = \frac{4n}{2^{S/2}} + \sqrt{\frac{1}{2^S}} = \frac{1}{2^{S/2}}(4n + 1) $. Finally, we can conclude the proof by using <ref> and <ref> that directly show that this protocol realizes $\Verif^f$ and can be turned, with little changes, into a protocol realizing $\Verif$.

§.§ Graph state verification

The work of <cit.> presents a generalization of the previous protocol to arbitrary graph states, where the verifier will ask parties to measure random stabilizers of the graph state. We can similarly show that it is composably secure. Note however that this protocol, like the previous one, shows security scaling polynomially with the security parameter while we usually expect it to scale super-polynomially. However, this allows significantly simpler protocols and most existing graph state verification protocols have this property. But our framework, of course, also applies to protocols that are super-polynomially secure.

[][end, restate]
We define, as in the theorem 3 of  <cit.> (where we use the fact that conditioned on non-aborting, we have $N_{\mathsf{pass}} \geq \lambda J N_{\mathsf{test}} - \frac{N_{\mathsf{test}}}{2J}$ as described in protocol 2 to simplify the expression of $p_0$ and avoid any dependency on a number that might be different every time we run the protocol):

* $J = 2^n$ or $J = n$ depending on $G$ as described in <cit.>,

* $\lambda$ be the security parameter growing polynomially with the number of tests

* $m$ and $c$ some positive constants chosen so that $p_0$ and $\eta_0$ defined later are greater than $0$,

* $p_0 \eqdef [1-\sum_{x=0}^\lambda (1-\frac{1}{n})^x(\frac{1}{n} J^{\frac{-2cm}{3}})^{\lambda-x}]^J$ (we got rid of the number of honest parties $|H| \geq 1$ since we want this to be independent of the number of malicious parties)

* $\eta_0 \eqdef \left(\frac{1}{\lambda} - \frac{1}{\lambda^2} \right) + \left(1+\frac{1}{\lambda} \right)\frac{\sqrt{c}+1/2}{J}$

The symmetric protocol 2 defined in <cit.>, assuming that we use a broadcast channel to transmit the abort bit, is an $\eps$-graph state verification protocol for $\eps \eqdef 1 - p_0 + 2\eta_0-\eta_0^2$. As a result, it $(2\sqrt{2\eps - \eps^2})$-realizes $\Verif[\ket{G}]^f$ as defined in <ref>, and can be turned into a protocol that $(2\sqrt{2\eps - \eps^2})$-realizes $\Verif$.

This is mostly a corollary of <ref>, using the first version of the assumption (<ref>). Indeed, using <cit.>, and by denoting by $\rho_i$ the reduced state outputted by honest parties during a given run (this corresponds to $\rho_H^{\mathsf{avg}}$ in <cit.>), we know that for any adversary $\cA$:

\begin{align}
\pr[\rho_i \gets \Tr_{[n] \setminus H} \pi_H \cR \cA, \rho_i \neq \ket{\bot^{H}}]{F(\rho_i, \Tr_{[n] \setminus H}\ketbra{G}{G}) \geq 1-\eta_0} \geq p_0
\end{align}

But for any $\rho_i$,

\begin{align}
F(\rho_i, \Tr_{[n] \setminus H}\ketbra{G}{G}) \geq 1-\eta_0
\Leftrightarrow
\sqrt{1-F^2(\rho_i, \Tr_{[n] \setminus H}\ketbra{G}{G})} \leq \sqrt{1-(1-\eta_0)^2} = \sqrt{2\eta_0-\eta_0^2}
\end{align}

So let $\eta \eqdef \sqrt{2\eta_0-\eta_0^2}$, and $\delta \eqdef 1 - p_0$. We have therefore:

\begin{align}
\pr[\rho_i \gets \Tr_{[n] \setminus H} \pi_H \cR \cA, \rho_i \neq \ket{\bot^{H}}]{\sqrt{1-F^2(\rho_i, \Tr_{[n] \setminus H}\ketbra{G}{G})} \geq \eta_0} \leq \delta
\end{align}

and, since $\pr{X \land E} = \pr[E]{x} \pr{E} \leq \pr[E]{x}$, we get as well:

\begin{align}
\pr[\rho_i \gets \Tr_{[n] \setminus H} \pi_H \cR \cA]{\rho_i \neq \ket{\bot^{H}} \land \sqrt{1-F^2(\rho_i, \Tr_{[n] \setminus H}\ketbra{G}{G})} \leq \eta_0} \leq \delta
\end{align}

So according to <ref>, the protocol is an $(\delta + \eta^2)$-graph state verification protocol, i.e. an $\eps$-graph state verification protocol for $\eps \eqdef \delta + \eta^2 = 1 - p_0 + 2\eta_0-\eta_0^2$. Finally, we can conclude the proof by using <ref> and <ref> that directly show that this protocol realizes $\Verif^f$ and can be turned, with little changes, into a protocol realizing $\Verif$.

§ CONCLUSION

In this work, we studied the composable security of generic graph-state verification protocols, i.e. protocols consisting of a source sharing graph-states to a network of parties, who then only perform local operations and classical communications, to decide whether they can use some of the states for another protocol. We showed that they can be considered equivalent to an ideal abstract resource, up to an $\eps$ that we explicited. This resource shares graph-states while allowing a restricted class of corrections to be applied to them by malicious parties. We proved that without modifying the original protocols, these malicious actions cannot be prevented when considering generic black-box simulators. We thus showed how to modify the original verification protocols to prevent the malicious parties to effectively act on the shared graph-state. The modification consists in asking the parties to jointly apply a random stabilizer to the state that they receive. By doing so, the modified protocol can be considered equivalent to a ideal functionality simply sharing graph-states. In this modified version, the dishonest parties can only force the protocol to abort.

To prove our results, we studied the class of mergeable states, to which graph-states belongs. We showed that we can merge two copies of a graph state into one copy, by acting only on a partition of the qubits. This generalizes entanglement swapping to arbitrary graph state. We explicited the measurements and local operations to do this swapping using scalable ZX-calculus <cit.>. For graph-state manipulation, the scalable ZX-calculus formalism proved to be more handy than the usual density matrix formalism, and we provide an introduction in <ref>. We believe this work is one of the first using such methods in the context of quantum cryptography.

We emphasize that our results mostly preserves the security features of the original protocol. Notably, if the initial protocol is $\eps$-secure, our claim is that it $\eps'$-realizes the above functionalities where $\eps'$ is polynomially related to $\eps$. In particular, if $\eps$ is scaling inverse polynomially with the security parameter, $\eps'$ will also scale inverse polynomially. On the other hand if $\eps$ is negligible, so will $\eps'$.

Our results are crucial in the context of network protocol development. The class of verification protocols that we studied are use as building-blocks in many quantum network protocols. Our work explicits to which extent they can be repeatedly used by computing of communication protocols to get verified graph-state without threatening the overall security. We showed in the last section of the paper how to apply our result to two existing verification protocols <cit.>. In the process, we answered negatively a conjecture posed in <cit.> stating that graph-state verification protocols cannot be proven composably secure in the Abstract cryptography framework. Moreover, our composability proof readily applies in a network where trusted parties wish to build trust on a source of graph-state. This is the case in many real-life scenario where a group of people wish to get a graph-state from an untrusted network to perform, for example, a multiparty computing protocol. In future works, we will study different contexts in which our result can apply.

§ ACKNOWLEDGMENT

The authors deeply thank Robert Booth for suggesting a more elegant representation of graph states. This work is co-funded by the European Union (ERC, ASC-Q, 101040624) and the Horizon Europe program (QUCATS). It is also supported by the Dutch National Growth Fund (NGF), as part of the Quantum Delta NL programme, and the Government of Spain (Severo Ochoa CEX2019-000910-S and FUNQIP), Fundació Cellex, Fundació Mir-Puig, Generalitat de Catalunya (CERCA program). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. This work is supported by France 2030 under the French National Research Agency projects HQI ANR-22-PNCQ-0002 and EPiQ ANR-22-PETQ-0007 as well as ANR Project SecNISQ. Neither the European Union nor the granting authority can be held responsible for them.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

abstractForty years ago, Wiesner proposed using quantum states to create money that is physically impossible to counterfeit, something that cannot be done in the classical world. However, Wiesner's scheme required a central bank to verify the money, and the question of whether there can be unclonable quantum money that anyone can verify has remained open since. One can also ask a related question, which seems to be new: can quantum states be used as copy-protected programs, which let the user evaluate some function f, but not create more programs for f? This paper tackles both questions using the arsenal of modern computational complexity. Our main result is that there exist quantum oracles relative to which publicly-verifiable quantum money is possible, and any family of functions that cannot be efficiently learned from its input-output behavior can be quantumly copy-protected. This provides the first formal evidence that these tasks are achievable. The technical core of our result is a "Complexity-Theoretic No-Cloning Theorem," which generalizes both the standard No-Cloning Theorem and the optimality of Grover search, and might be of independent interest. Our security argument also requires explicit constructions of quantum t-designs. Moving beyond the oracle world, we also present an explicit candidate scheme for publicly-verifiable quantum money, based on random stabilizer states; as well as two explicit schemes for copy-protecting the family of point functions. We do not know how to base the security of these schemes on any existing cryptographic assumption. (Note that without an oracle, we can only hope for security under some computational assumption).
booktitle2009 24th Annual IEEE Conference on Computational Complexity
eventtitle2009 24th Annual IEEE Conference on Computational Complexity
titleQuantum Copy-Protection and Quantum Money

American Physical Society

journaltitlePhysical Review Letters
shortjournalPhys. Rev. Lett.
titleTeleporting an Unknown Quantum State via Dual Classical and Einstein-Podolsky-Rosen Channels

Springer Science
Business Media LLC

journaltitleNature Physics
titleMeasurement-based quantum computation

titleQuantum weak coin flipping with a single photon

abstractWe present a protocol which allows a client to have a server carry out a quantum computation for her such that the client's inputs, outputs and computation remain perfectly private, and where she does not require any quantum computational power or memory. The client only needs to be able to prepare single qubits randomly chosen from a finite set and send them to the server, who has the balance of the required quantum computational resources. Our protocol is interactive: after the initial preparation of quantum states, the client and server use two-way classical communication which enables the client to drive the computation, giving single-qubit measurement instructions to the server, depending on previous measurement outcomes. Our protocol works for inputs and outputs that are either classical or quantum. We give an authentication protocol that allows the client to detect an interfering server; our scheme can also be made fault-tolerant. We also generalize our result to the setting of a purely classical client who communicates classically with two non-communicating entangled servers, in order to perform a blind quantum computation. By incorporating the authentication protocol, we show that any problem in BQP has an entangled two-prover interactive proof with a purely classical verifier. Our protocol is the first universal scheme which detects a cheating server, as well as the first protocol which does not require any quantum computation whatsoever on the client's side. The novelty of our approach is in using the unique features of measurement-based quantum computing which allows us to clearly distinguish between the quantum and classical aspects of a quantum computation.
booktitle2009 50th Annual IEEE Symposium on Foundations of Computer Science
eventtitle2009 50th Annual IEEE Symposium on Foundations of Computer Science
titleUniversal Blind Quantum Computation
Authentication,Computer aided instruction,Computer science,Fault detection,Fault tolerance,Informatics,measurement-based quantum computing,Privacy,Protocols,Quantum,Quantum computing,quantum cryptography,Quantum entanglement,quantum prover interactive proofs

Springer Science
Business Media LLC

journaltitlenpj Quantum Information
titleExperimental investigation of practical unforgeable quantum money

abstractWe propose a novel paradigm for defining security of cryptographic protocols, called universally composable security. The salient property of universally composable definitions of security is that they guarantee security even when a secure protocol is composed of an arbitrary set of protocols, or more generally when the protocol is used as a component of an arbitrary system. This is an essential property for maintaining security of cryptographic protocols in complex and unpredictable environments such as the Internet. In particular, universally composable definitions guarantee security even when an unbounded number of protocol instances are executed concurrently in an adversarially controlled manner, they guarantee non-malleability with respect to arbitrary protocols, and more. We show how to formulate universally composable definitions of security for practically any cryptographic task. Furthermore, we demonstrate that practically any such definition can be realized using known techniques, as long as only a minority of the participants are corrupted. We then proceed to formulate universally composable definitions of a wide array of cryptographic tasks, including authenticated and secure communication, key-exchange, public-key encryption, signature, commitment, oblivious transfer, zero knowledge and more. We also make initial steps towards studying the realizability of the proposed definitions in various settings.
booktitleProceedings 42nd IEEE Symposium on Foundations of Computer Science
eventtitleProceedings 42nd IEEE Symposium on Foundations of Computer Science
shorttitleUniversally Composable Security
titleUniversally Composable Security: A New Paradigm for Cryptographic Protocols
Application software,Computer science,Computer security,Cryptographic protocols,Cryptography,Job design,Mathematical model,Radio access networks,Reactive power

abstractThis note describes how the the scalable ZXH calculus can be used to represent in a compact way the quantum gates that are diagonal in the computational basis. This includes controlled and multi-controlled Z gates, their generalizations, respectively graph and hypergraph operators, and also phase gadgets.
titleA Note on Diagonal Gates in SZX-calculus

Berlin, Heidelberg

abstractWe formalise the constructive content of an essential feature of quantum mechanics: the interaction of complementary quantum observables, and information flow mediated by them. Using a general categorical formulation, we show that pairs of mutually unbiased quantum observables form bialgebra-like structures. We also provide an abstract account on the quantum data encoded in complex phases, and prove a normal form theorem for it. Together these enable us to describe all observables of finite dimensional Hilbert space quantum mechanics. The resulting equations suffice to perform computations with elementary quantum gates, translate between distinct quantum computational models, establish the equivalence of entangled quantum states, and simulate quantum algorithms such as the quantum Fourier transform. All these computations moreover happen within an intuitive diagrammatic calculus.
booktitleAutomata, Languages and Programming
seriesLecture Notes in Computer Science
titleInteracting Quantum Observables
Bloch Sphere,Classical Point,Classical Structure,Monoidal Structure,Quantum Observable

journaltitlePhys. Rev. Applied
titlePractical quantum electronic voting

abstractWe introduce the Scalable ZX-calculus (SZX-calculus for short), a formal and compact graphical language for the design and verification of quantum computations. The SZX-calculus is an extension of the ZX-calculus, a powerful framework that captures graphically the fundamental properties of quantum mechanics through its complete set of rewrite rules. The ZX-calculus is, however, a low level language, with each wire representing a single qubit. This limits its ability to handle large and elaborate quantum evolutions. We extend the ZX-calculus to registers of qubits and allow compact representation of sub-diagrams via binary matrices. We show soundness and completeness of the SZX-calculus and provide two examples of applications, for graph states and error correcting codes.
titleSZX-calculus: Scalable Graphical Quantum Reasoning
pages15 pages

Cambridge University Press

abstractThe unique features of the quantum world are explained in this book through the language of diagrams, setting out an innovative visual method for presenting complex theories. Requiring only basic mathematical literacy, this book employs a unique formalism that builds an intuitive understanding of quantum features while eliminating the need for complex calculations. This entirely diagrammatic presentation of quantum theory represents the culmination of ten years of research, uniting classical techniques in linear algebra and Hilbert spaces with cutting-edge developments in quantum computation and foundations. Written in an entertaining and user-friendly style and including more than one hundred exercises, this book is an ideal first course in quantum theory, foundations, and computation for students from undergraduate to PhD level, as well as an opportunity for researchers from a broad range of fields, from physics to biology, linguistics, and cognitive science, to discover a new set of tools for studying processes and interaction.
shorttitlePicturing Quantum Processes
titlePicturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning

abstractWe provide a generic construction to turn any classical Zero-Knowledge (ZK) protocol into a composable (quantum) oblivious transfer (OT) protocol, mostly lifting the round-complexity properties and security guarantees (plain-model/statistical security/unstructured functions...) of the ZK protocol to the resulting OT protocol. Such a construction is unlikely to exist classically as Cryptomania is believed to be different from Minicrypt. In particular, by instantiating our construction using Non-Interactive ZK (NIZK), we provide the first round-optimal (2-message) quantum OT protocol secure in the random oracle model, and round-optimal extensions to string and k-out-of-n OT. At the heart of our construction lies a new method that allows us to prove properties on a received quantum state without revealing (too much) information on it, even in a non-interactive way and/or with statistical guarantees when using an appropriate classical ZK protocol. We can notably prove that a state has been partially measured (with arbitrary constraints on the set of measured qubits), without revealing any additional information on this set. This notion can be seen as an analog of ZK to quantum states, and we expect it to be of independent interest as it extends complexity theory to quantum languages, as illustrated by the two new complexity classes we introduce, ZKstateQIP and ZKstateQMA.
noteTo appear in ASIACRYPT 2023
titleOblivious Transfer from Zero-Knowledge Proofs, or How to Achieve Round-Optimal Quantum Oblivious Transfer and Zero-Knowledge Proofs on Quantum States
81-XX,Computer Science - Cryptography and Security,Quantum Physics

Berlin, Heidelberg

abstractWe consider the problem of hiding sender and receiver of classical and quantum bits (qubits), even if all physical transmissions can be monitored. We present a quantum protocol for sending and receiving classical bits anonymously, which is completely traceless: it successfully prevents later reconstruction of the sender. We show that this is not possible classically. It appears that entangled quantum states are uniquely suited for traceless anonymous transmissions. We then extend this protocol to send and receive qubits anonymously. In the process we introduce a new primitive called anonymous entanglement, which may be useful in other contexts as well.
booktitleAdvances in Cryptology - ASIACRYPT 2005
seriesLecture Notes in Computer Science
titleQuantum Anonymous Transmissions
leo/Zotero/storage/VV96D4H5/Christandl et Wehner - 2005 - Quantum Anonymous Transmissions.pdf
Broadcast Channel,Byzantine Agreement,Classical Protocol,Collision Detection,Quantum Protocol

Springer International Publishing

abstractThe cryptographic task of secure multi-party (classical) computation has received a lot of attention in the last decades. Even in the extreme case where a computation is performed between k mutually distrustful players, and security is required even for the single honest player if all other players are colluding adversaries, secure protocols are known. For quantum computation, on the other hand, protocols allowing arbitrary dishonest majority have only been proven for k=2k=2k=2. In this work, we generalize the approach taken by Dupuis, Nielsen and Salvail (CRYPTO 2012) in the two-party setting to devise a secure, efficient protocol for multi-party quantum computation for any number of players k, and prove security against up to k−1k−1k-1 colluding adversaries. The quantum round complexity of the protocol for computing a quantum circuit of {CNOT,T}{CNOT,T}\{\mathsf {CNOT}, \mathsf {T} \} depth d is O(k⋅(d+logn))O(k⋅(d+logn))O(k \cdot (d + \log n)), where n is the security parameter. To achieve efficiency, we develop a novel public verification protocol for the Clifford authentication code, and a testing protocol for magic-state inputs, both using classical multi-party computation.
booktitleAdvances in Cryptology – EUROCRYPT 2020
seriesLecture Notes in Computer Science
titleSecure Multi-party Quantum Computation with a Dishonest Majority

Berlin, Heidelberg

abstractWe provide the first two-party protocol allowing Alice and Bob to evaluate privately even against active adversaries any completely positive, trace-preserving map F∈L(Ain⊗Bin)→F∈L(Ain⊗Bin)→\mathscr {F} \in \mathrm {L}(\mathcal {A}_{{{\mathrm{in}}}} \otimes \mathcal {B}_{{{\mathrm{in}}}}) \rightarrow L(Aout⊗Bout)L(Aout⊗Bout)\mathrm {L}(\mathcal {A}_{{{\mathrm{out}}}} \otimes \mathcal {B}_{{{\mathrm{out}}}}), given as a quantum circuit, upon their joint quantum input state ρin∈D(Ain⊗Bin)ρin∈D(Ain⊗Bin)\rho _{\mathrm {in}}\in \mathrm{D}({\mathcal {A}_{{{\mathrm{in}}}} \otimes \mathcal {B}_{{{\mathrm{in}}}}}). Our protocol leaks no more to any active adversary than an ideal functionality for FF\mathscr {F} provided Alice and Bob have the cryptographic resources for active secure two-party classical computation. Our protocol is constructed from the protocol for the same task secure against specious adversaries presented in [4].
booktitleAdvances in Cryptology – CRYPTO 2012
seriesLecture Notes in Computer Science
titleActively Secure Two-Party Evaluation of Any Quantum Operation
Active Security,Authentication Code,Ideal Functionality,QMPC,Quantum Circuit,Quantum Operation

American Physical Society

abstractBlind quantum computing (BQC) allows a client to have a server carry out a quantum computation for them such that the client's input, output, and computation remain private. A desirable property for any BQC protocol is verification, whereby the client can verify with high probability whether the server has followed the instructions of the protocol or if there has been some deviation resulting in a corrupted output state. A verifiable BQC protocol can be viewed as an interactive proof system leading to consequences for complexity theory. We previously proposed [A. Broadbent, J. Fitzsimons, and E. Kashefi, in Proceedings of the 50th Annual Symposium on Foundations of Computer Science, Atlanta, 2009 (IEEE, Piscataway, 2009), p. 517] a universal and unconditionally secure BQC scheme where the client only needs to be able to prepare single qubits in separable states randomly chosen from a finite set and send them to the server, who has the balance of the required quantum computational resources. In this paper we extend that protocol with additional functionality allowing blind computational basis measurements, which we use to construct another verifiable BQC protocol based on a different class of resource states. We rigorously prove that the probability of failing to detect an incorrect output is exponentially small in a security parameter, while resource overhead remains polynomial in this parameter. This resource state allows entangling gates to be performed between arbitrary pairs of logical qubits with only constant overhead. This is a significant improvement on the original scheme, which required that all computations to be performed must first be put into a nearest-neighbor form, incurring linear overhead in the number of qubits. Such an improvement has important consequences for efficiency and fault-tolerance thresholds.
journaltitlePhysical Review A
shortjournalPhys. Rev. A
titleUnconditionally Verifiable Blind Quantum Computation

journaltitleQuantum Information Processing
titleQuantum Leader Election

abstractQuantum computers promise to efficiently solve not only problems believed to be intractable for classical computers, but also problems for which verifying the solution is also considered intractable. This raises the question of how one can check whether quantum computers are indeed producing correct results. This task, known as quantum verification, has been highlighted as a significant challenge on the road to scalable quantum computing technology. We review the most significant approaches to quantum verification and compare them in terms of structure, complexity and required resources. We also comment on the use of cryptographic techniques which, for many of the presented protocols, has proven extremely useful in performing verification. Finally, we discuss issues related to fault tolerance, experimental implementations and the outlook for future protocols.
journaltitleTheory of Computing Systems
shortjournalTheory Comput Syst
shorttitleVerification of Quantum Computation
titleVerification of Quantum Computation: An Overview of Existing Approaches

Springer International Publishing

abstractMiniQCrypt is a world where quantum-secure one-way functions exist, and quantum communication is possible. We construct an oblivious transfer (OT) protocol in MiniQCrypt that achieves simulation-security in the plain model against malicious quantum polynomial-time adversaries, building on the foundational work of Crépeau and Killian (FOCS 1988) and Bennett, Brassard, Crépeau and Skubiszewska (CRYPTO 1991). Combining the OT protocol with prior works, we obtain secure two-party and multi-party computation protocols also in MiniQCrypt. This is in contrast to the classical world, where it is widely believed that one-way functions alone do not give us OT.In the common random string model, we achieve a constant-round universally composable (UC) OT protocol.
booktitleAdvances in Cryptology – EUROCRYPT 2021
seriesLecture Notes in Computer Science
titleOblivious Transfer Is in MiniQCrypt
leo/Zotero/storage/9JEE5DC9/Grilo et al. - 2021 - Oblivious Transfer Is in MiniQCrypt.pdf

abstractThe privacy of communicating participants is often of paramount importance, but in some situations it is an essential condition. A typical example is a fair (secret) voting. We analyze in detail communication privacy based on quantum resources, and we propose new quantum protocols. Possible generalizations that would lead to voting schemes are discussed.
journaltitlePhysics Letters A
shortjournalPhysics Letters A
titleTowards Quantum-Based Privacy and Voting

titleMultiparty Delegated Quantum Computing

Springler Berlin Heidelberg

journaltitleIN Theory of Security and Applications
titleConstructive Cryptography - A New Paradigm for Security Definitions and Proofs

Berlin, Heidelberg

abstractConstructive cryptography, an application of abstract cryptography proposed by Maurer and Renner, is a new paradigm for defining the security of cryptographic schemes such as symmetric encryption, message authentication codes, public-key encryption, key-agreement protocols, and digital signature schemes, and for proving the security of protocols making use of such schemes. Such a cryptographic scheme can be seen (and defined) as constructing a certain resource (e.g. a channel or key) with certain security properties from another (weaker) such resource. For example, a secure encryption scheme constructs a secure channel from an authenticated channel and a secret key.The term “construct”, which is defined by the use of a simulator, is composable in the sense that a protocol obtained by the composition of several secure constructive steps is itself secure. This is in contrast to both the traditional, game-based security definitions for cryptographic schemes and the attack-based security definitions used in formal-methods based security research, which are generally not composable.Constructive cryptography allows to take a new look at cryptography and the design of cryptographic protocols. One can give explicit meaning to various types of game-based security notions of confidentiality, integrity, and malleability, one can design key agreement, secure communication, certification, and other protocols in a modular and composable manner, and one can separate the understanding of what cryptography achieves from the technical security definitions and proofs, which is useful for didactic purposes and protocol design.
booktitleTheory of Security and Applications
seriesLecture Notes in Computer Science
titleConstructive Cryptography – A New Paradigm for Security Definitions and Proofs
Cryptographic Scheme,Digital Signature Scheme,Message Authentication Code,Secure Channel,Security Proof

abstractWe propose a simple protocol for the verification of quantum computation after the computation has been performed. Our construction can be seen as an improvement on previous results in that it requires only a single prover, who is restricted to measuring qubits in the $X$ or $Z$ basis, while requiring only one way communication, from the prover to the verifier. We also show similar constant round protocols with purely classical verifiers are not possible, unless BQP is contained in the third level of the polynomial hierarchy.
issn0031-9007, 1079-7114
journaltitlePhysical Review Letters
shortjournalPhys. Rev. Lett.
titlePost Hoc Verification with a Single Prover
8 - Post hoc verification with a single prover.pdf;/home/leo/Zotero/storage/ZPYW523A/1603.html

journaltitleNature Communications
titleExperimental Verification of Multipartite Entanglement in Quantum Networks

abstractA general framework for defining and proving that a system satisfying an (abstract or ideal) specification is constructed from some systems satisfying certain (concrete or real) specifications is proposed, applicable in various cryptographic settings. Cryptography Ueli Maurer Renato Renner Department of Computer Science, ETH Zurich, Switzerland Institute for Theoretical Physics, ETH Zurich, Switzerland<EMAIL_ADDRESS><EMAIL_ADDRESS>Abstract: In the spirit of algebraic abstraction, this paper advocates the definition and use of higher levels of abstraction in cryptography (and beyond). If contrasted with the standard bottom-up approach to defining models of computation, algorithms, complexity, efficiency, and then security of cryptographic schemes, our approach is top-down and axiomatic, where lower abstraction levels inherit the definitions and theorems (e.g. a composition theorem) from the higher level, but the definition or concretization of low levels is not required for proving theorems at the higher levels. The goal is to strive for simpler definitions, higher generality of results, simpler proofs, improved elegance, possibly better didactic suitability, and to derive new insights from the abstract viewpoint. In particular, we propose a general framework for defining and proving that a system satisfying an (abstract or ideal) specification is constructed from some systems satisfying certain (concrete or real) specifications. This puts the well-known “ideal-world real-world” paradigm on a new theoretical foundation, applicable in various cryptographic settings. Existing frameworks for proving composable security can be explained as special cases of our framework, thereby allowing to distinguish between relevant and less relevant aspects of the underlying technical definitions and to prove a single common composition theorem. Some properties of our framework are as follows. It is independent of particular models of computation, communication, and adversary behavior. It can be instantiated in many different ways, for example to arrive at different notions of security or of efficiency and infeasibility. It can precisely capture settings with no central adversary where entities have potentially conflicting goals (e.g. a coercion scenario). The relation between the ideal and the real setting is tight, via an isomorphism notion for settings. The (desired) asymmetry between real and ideal is captured in a formal abstraction notion (the ideal setting is an abstraction of the real setting). A main theorem states that such an abstraction statement can be proved by using local (as opposed to monolithic) simulators. In the spirit of algebraic abstraction, this paper advocates the definition and use of higher levels of abstraction in cryptography (and beyond). If contrasted with the standard bottom-up approach to defining models of computation, algorithms, complexity, efficiency, and then security of cryptographic schemes, our approach is top-down and axiomatic, where lower abstraction levels inherit the definitions and theorems (e.g. a composition theorem) from the higher level, but the definition or concretization of low levels is not required for proving theorems at the higher levels. The goal is to strive for simpler definitions, higher generality of results, simpler proofs, improved elegance, possibly better didactic suitability, and to derive new insights from the abstract viewpoint. In particular, we propose a general framework for defining and proving that a system satisfying an (abstract or ideal) specification is constructed from some systems satisfying certain (concrete or real) specifications. This puts the well-known “ideal-world real-world” paradigm on a new theoretical foundation, applicable in various cryptographic settings. Existing frameworks for proving composable security can be explained as special cases of our framework, thereby allowing to distinguish between relevant and less relevant aspects of the underlying technical definitions and to prove a single common composition theorem. Some properties of our framework are as follows. It is independent of particular models of computation, communication, and adversary behavior. It can be instantiated in many different ways, for example to arrive at different notions of security or of efficiency and infeasibility. It can precisely capture settings with no central adversary where entities have potentially conflicting goals (e.g. a coercion scenario). The relation between the ideal and the real setting is tight, via an isomorphism notion for settings. The (desired) asymmetry between real and ideal is captured in a formal abstraction notion (the ideal setting is an abstraction of the real setting). A main theorem states that such an abstraction statement can be proved by using local (as opposed to monolithic) simulators.
titleAbstract Cryptography

Tsinghua University Press

journaltitleIn Innovations In Computer Science
titleAbstract cryptography

Berlin, Heidelberg

Springer Berlin Heidelberg

booktitleTheory of Cryptography
titleFrom Indifferentiability to Constructive Cryptography (and Back)

Higher Education from Cambridge University Press

Cambridge University Press

abstractOne of the most cited books in physics of all time, Quantum Computation and Quantum Information remains the best textbook in this exciting field of science. This 10th anniversary edition includes an introduction from the authors setting the work in context. This comprehensive textbook describes such remarkable effects as fast quantum algorithms, quantum teleportation, quantum cryptography and quantum error-correction. Quantum mechanics and computer science are introduced before moving on to describe what a quantum computer is, how it can be used to solve problems faster than 'classical' computers and its real-world implementation. It concludes with an in-depth treatment of quantum information. Containing a wealth of figures and exercises, this well-known textbook is ideal for courses on the subject, and will interest beginning graduate students and researchers in physics, computer science, mathematics, and electrical engineering.
shorttitleQuantum Computation and Quantum Information
titleQuantum Computation and Quantum Information: 10th Anniversary Edition

journaltitlePhysical Review Letters
titleMultipartite Entanglement Verification Resistant against Dishonest Parties

American Physical Society

journaltitlePhysical Review A
shortjournalPhys. Rev. A
titleVerification of Graph States in an Untrusted Network

journaltitlePhysical Review Letters
titleAnonymity for practical quantum networks

Berlin, Heidelberg

abstractThe Universal Composability model (UC) by Canetti (FOCS 2001) allows for secure composition of arbitrary protocols. We present a quantum version of the UC model which enjoys the same compositionality guarantees. We prove that in this model statistically secure oblivious transfer protocols can be constructed from commitments. Furthermore, we show that every statistically classically UC secure protocol is also statistically quantum UC secure. Such implications are not known for other quantum security definitions. As a corollary, we get that quantum UC secure protocols for general multi-party computation can be constructed from commitments.
booktitleAdvances in Cryptology – EUROCRYPT 2010
seriesLecture Notes in Computer Science
titleUniversally Composable Quantum Multi-party Computation
leo/Zotero/storage/CRWSJ64W/Unruh - 2010 - Universally Composable Quantum Multi-party Computa.pdf
Commitment Scheme,Computational Basis,Oblivious Transfer,Quantum Protocol,Quantum Setting
family=van de Wetering,

abstractThe ZX-calculus is a graphical language for reasoning about quantum computation that has recently seen an increased usage in a variety of areas such as quantum circuit optimisation, surface codes and lattice surgery, measurement-based quantum computation, and quantum foundations. The first half of this review gives a gentle introduction to the ZX-calculus suitable for those familiar with the basics of quantum computing. The aim here is to make the reader comfortable enough with the ZX-calculus that they could use it in their daily work for small computations on quantum circuits and states. The latter sections give a condensed overview of the literature on the ZX-calculus. We discuss Clifford computation and graphically prove the Gottesman-Knill theorem, we discuss a recently introduced extension of the ZX-calculus that allows for convenient reasoning about Toffoli gates, and we discuss the recent completeness theorems for the ZX-calculus that show that, in principle, all reasoning about quantum computation can be done using ZX-diagrams. Additionally, we discuss the categorical and algebraic origins of the ZX-calculus and we discuss several extensions of the language which can represent mixed states, measurement, classical control and higher-dimensional qudits.
journaltitlearXiv:2012.13966 [quant-ph]
titleZX-calculus for the Working Quantum Computer Scientist
Not published,Quantum Physics,Reviews,ZX-Calculus

journaltitleACM SIGACT News
shortjournalSIGACT News
titleConjugate Coding

issn2469-9926, 2469-9934
journaltitlePhysical Review A
shortjournalPhys. Rev. A
titleComposable Security for Multipartite Entanglement Verification
Introduction to the (scalable) ZX-calculus

§.§ Introduction to the (scalable) ZX-calculus.

A ZX-diagram is a graph with some inputs (on the left) and outputs (on the right). We can associate to any ZX-diagram a matrix, using the following interpretation of the generators, where the colored nodes are being called “spiders”, and $H$ being strictly speaking only a syntactic sugar:

\begin{align*}
\begin{split}
% Green spider
\left\llbracket\, \zx{\leftManyDots{n} \zxZ{\alpha} \rightManyDots{m}} \,\right\rrbracket &= \ket{0}^{\otimes m}\bra{0}^{\otimes n}+e^{i \alpha}\ket{1}^{\otimes m}\bra{1}^{\otimes n}\\
% Red spider
\left\llbracket\, \zx{\leftManyDots{n} \zxX{\alpha} \rightManyDots{m}} \,\right\rrbracket &= \ket{+}^{\otimes m}\bra{+}^{\otimes n}+e^{i \alpha}\ket{-}^{\otimes m}\bra{-}^{\otimes n}\\
% Swap
\left\llbracket\,
\begin{ZX}
\zxN{} \ar[rd,s] &[\zxWCol] \zxN{}\\[\zxWCol]
\zxN{} \ar[ru,s] &[\zxWCol] \zxN{}
\end{ZX}
\,\right\rrbracket &= \ketbra{00}{00}+\ketbra{10}{01}+\ketbra{01}{10}+\ketbra{11}{11}\\
% H
\left\llbracket\,\zx{\zxNone{} \rar &[\zxwCol] \zxH{} \rar &[\zxwCol] \zxNone{}}\,\right\rrbracket &= \ketbra{+}{0}+\ketbra{-}{1}
\end{split}%\qquad
\begin{split}
% Wire
\left\llbracket\, \zx{\zxNone{} \rar &[2mm] \zxNone{}} \,\right\rrbracket  &= \ketbra{0}{0}+\ketbra{1}{1}\\
% Bell preparation
\left\llbracket\,\zx{\zxN{} \dar[C]\\[\zxWCol] \zxN{}}\,\right\rrbracket &= \ket{00}+\ket{11}\\
% Bell projection
\left\llbracket\,\zx{\zxN{} \dar[C-]\\[\zxWCol] \zxN{}}\,\right\rrbracket &= \bra{00}+\bra{11}\\
% Empty
\llbracket\, \zx[inner sep=1mm]{\zxEmptyDiagram{}} \,\rrbracket &= \begin{pmatrix} 1 \end{pmatrix}
\end{split}
\end{align*}

Note that when $\alpha = 0$, we can omit the angle in the spiders. Moreover, we can compose these generators sequentially (resp. in parallel). We then obtain the resulting natural interpretation, by inductively computing the matrix product (resp. tensor product) of the interpretation of the sub-diagrams.

Circuit to ZX.

One can turn any quantum circuit into a ZX-diagram. Let $(a,b) \in \{0,1\}^2$ and $\alpha \in \R$. Then, up to a non-relevant re-normalisation scalar and global phase, we represent basic states using $\zx{\zxX*{a\pi} \rar &[\zxwCol]} = \ket{a}$, $\zx{\zxZ*{a\pi} \rar &[\zxwCol]} = H\ket{a}$ and one-qubits gates using $\zx{\zxNL \zxH{} \zxNR} = \gateH$, $\zx{\zxN{} \rar &[\zxwCol] \zxX{\alpha} \rar &[\zxwCol] \zxN{}} = \gateRX(\alpha)$ and $\zx{\zxN{} \rar &[\zxwCol] \zxZ{\alpha} \rar &[\zxwCol] \zxN{}} = \gateRZ(\alpha)$. We have in particular $\zx{\zxN{} \rar &[\zxwCol] \zxX*{a\pi} \rar &[\zxwCol] \zxN{}} = \gateX^a$ and $\zx{\zxN{} \rar &[\zxwCol] \zxZ*{a\pi} \rar &[\zxwCol] \zxN{}} = \gateZ^a$. Two qubit gates are represented as[Although the generators do not allow vertical wires, we will see that we can freely bend wires and move nodes since “only topology matters”. We can therefore consider ZX-diagrams as undirected graphs.]
\zxN{} \rar &[\zxwCol] \zxZ{} \rar \dar &[\zxwCol] \zxN{}\\
\zxN{} \rar &[\zxwCol] \zxX{} \rar &[\zxwCol] \zxN{}
} = \gateCNOT$ and
\zxN{} \rar &[\zxwCol] \zxZ{} \rar \dar[H] &[\zxwCol] \zxN{}\\[\zxHRowFlat]
\zxN{} \rar &[\zxwCol] \zxZ{} \rar &[\zxwCol] \zxN{}
} = \gateCZ$. Moreover, we represent a measurement in the computational basis whose outcome is $a$ using $\zx{ \rar &[\zxwCol] \zxX*{a\pi}} = \bra{a}$ and a measurement in the Hadamard basis, i.e. the projection on $\ket{0} + (-1)^a\ket{1}$, whose outcome is $a$ $\zx{ \rar &[\zxwCol] \zxZ*{a\pi}} = \bra{a}H$ . Finally, $
\begin{ZX}
\rar & [\zxwCol] \zxZ*{a\pi} \dar[C-]\\
\rar & [\zxwCol] \zxX*{b\pi}\\
\end{ZX}
$ represents a Bell measurement (projection on $\ket{0b}+(-1)^a\ket{1\bar{b}}$) with outcomes $(a,b)$.

Scalable ZX.
The scalable ZX-calculus <cit.> generalises these generators: wires can be grouped (or ungrouped) together. We represent these grouped wires as bold wires, where we specify  above the number of wires in the group when there can be a confusion. The grouping/ungrouping of wires is done using so-called gatherers and dividers, shown in the first two diagrams of <ref> below. In scalable ZX, spiders can contain lists of real numbers, corresponding to stacked spiders, as we show for example in the two last diagram of <ref> with $\alpha \in \R$ and $\beta \in \R^{n-1}$:

\begin{align}
\label{eq:ScalableZxDef}
\begin{aligned}
% Defines divider
\begin{ZX}
\rar[Bn'Args={n}{pos=.9}] & [\zxWCol] \zxN{} \ar[dr, '>, B] & [\zxWCol]                        & [\zxWCol] \\[\zxZeroRow+.5mm]
&                                 & \zxDivider-{} \rar[wc,Bn'={n+m}] &           \\[\zxZeroRow+.5mm]
\rar[Bn.Args={m}{pos=.9}] & \zxN{} \ar[ur, .>, B]
\end{ZX}\qquad
% Defines gatherers
\begin{ZX}
& [\zxWCol]                                  & [\zxwCol] \zxN{} \rar[Bn'Args={n}{pos=.1}] & [\zxWCol] \\[\zxZeroRow+.5mm]
\rar[Bn'={n+m},wce] & \zxDivider{} \ar[B, dr, <.] \ar[ur, B, <'] &                                                        \\[\zxZeroRow+.5mm]
&                                            & \zxN{} \rar[Bn.Args={m}{pos=.1}]           &
\end{ZX}&\qquad\qquad
% Spiders as lists
\begin{ZX}
\zxN{} \rar[Bn'Args={n}{pos=.3},dr, '>, B] \ar[dd,3 vdots={$k$}] & [\zxWCol]                                                                                & [\zxWCol] \zxN{} \ar[dd,3 vdotsr={\footnotesize$l$}] \\[\zxZeroRow+.5mm]
& \zxZ[B]{\alpha{::}\beta} \ar[ru, <', Bn'Args={n}{pos=.7}] \ar[rd, <', Bn.Args={n}{pos=.7}] &                                                      \\[\zxZeroRow+.5mm]
\zxN{} \rar[Bn.Args={n}{pos=.3},ru, .>, B]                       &                                                                                & \zxN{}
\end{ZX}
\ \hypertarget{eq:zxRuleZ}{\eqAbove[\eqdef]{\myZXRule{Z}}}\ %
\begin{ZX}
\zxN{} \rar[B,wc,Bn'Args={n}{pos=.4}] \ar[d,3 vdots={$k$}] & [\zxwCol] \zxDivider{} \rar[] \ar[dr,B] & [\zxwCol] \zxZ{\alpha} \rar \ar[rd]  & [\zxwCol] \zxDivider-{} \rar[wc, Bn'Args={n}{pos=.6}] & [\zxwCol] \zxN{} \ar[d,3 vdotsr={$l$}] \\
\zxN{} \rar[B,wc,Bn.Args={n}{pos=.4}]                      & \zxDivider{} \rar[B] \ar[ur]            & \zxZ[B]{\beta} \ar[ru, B, wc] \ar[r, B] & \zxDivider-{} \rar[wc, Bn.Args={n}{pos=.6}]           & \zxN{}
\end{ZX}&\qquad\qquad
% Hadamard
\begin{ZX}[mbr]
\zxN{} \rar[Bn'Args={n+m}{}] &[\zxWCol+2mm] \zxH[B]{} \rar[Bn.Args={n+m}{}] &[\zxWCol+2mm] \zxN{}
\end{ZX}
\hypertarget{eq:zxRuleW}{\eqAbove[\eqdef]{\myZXRule{W}}}
\begin{ZX}[mbr=1]
\rar[B] & \zxDivider{} \ar[r,o',H={B},Bn'Args={n}{pos=.25}] \ar[r,o.,H={B},Bn.Args={m}{pos=.25}] &[\zxHCol+5mm] \zxDivider-{} \rar[B] &
\end{ZX}
% \begin{ZX}[mbr=2]
%           & [\zxwCol]                                    & [\zxwCol] \zxH{} \ar[rd,'>]    & [\zxwCol]\zxN{}       & [\zxwCol] \\[\zxZeroRow]
%   \rar[B] & \zxDivider{} \ar[ru,<'] \ar[rd,<.,Bn.={n-1}] &                                & \zxDivider-{} \rar[B] &           \\[\zxZeroRow]
%           &                                              & \zxH[B]{} \ar[ru,Bn.={n-1},.>] & [\zxWCol] \zxN{}
% \end{ZX}
\end{aligned}
\end{align}

The interest of the ZX-calculus is that we can rewrite a ZX diagram using some rewriting rules while preserving the interpretation of the corresponding matrix. The first rule is that only connectivity matters, i.e. we can bend wires arbitrarily as soon as the corresponding undirected graph is left unchanged. Other rules and theorems are described in <ref>. Note that, for simplicity, we will remove all scalars, i.e. sub-graphs having no input nor output, as they correspond to global phases (not observable physically) and/or a re-normalisation of the state.

Two diagrams composed only of identity, gatherers and dividers are equal iff their respective number of inputs and outputs are equal.

[a=a]                                [a=c]

[a=b]                                [a=myd]

[a=aa]                               [a=cc]

[a=bb]                               [a=mydd]

[from=a, to=alpha,'>,B]
[from=b, to=alpha,.>,B]
[to=c, from=alpha,<',B]
[from=a,to=b,3 vdots]
[from=c,to=myd,3 vdots]

[from=aa, to=beta,'>,B]
[from=bb, to=beta,.>,B]
[to=cc, from=beta,<',B]
[to=mydd, from=beta,<.,B]
[from=aa,to=bb,3 vdots]
[from=cc,to=mydd,3 vdots]

[from=alpha, to=beta, o-=-=.2,L=.3,B]
[from=alpha, to=beta, -o=-=.2,L=.3,B]
[from=alpha, to=beta, 3 dots]

[a=a]                                         [a=c]

[a=alpha,B]α+ β

[a=b]                                         [a=myd]

[from=a, to=alpha,'>,B]
[from=b, to=alpha,.>,B]
[to=c, from=alpha,<',B]
[from=a,to=b,3 vdots]
[from=c,to=myd,3 vdots]

[ampersand replacement=&]
&[]  &[]

[a=myb]     π2     π2     π2

[dd,3 vdots]                        []     []  [dd,3 vdots]

[B]α [B,ru,N'-,H=B,pos=.65]

[B,ru,-N',H=B,pos=.35]     []     []

[B,rd,-N.] [dd,3 vdots]     []                                  []  [dd,3 vdots]

[B]α [B,ru,N'-] [B,rd,N.-]

[B,ru,-N']                     []                                  []

[B]    [] [B] [B]    []

[B]    []

[] [a=a] [dd,3 vdots]

[B]*aπ [B]     [B,a=theta]θ

[from=theta, to=a,<',B]
[from=theta, to=b,<',B]

[a=a,B]*aπ [B]     [] [d,3 vdots] [B]

[a=b,B]*aπ [B]     []  [B]

[]                                              [a=a] [dd,3 vdots]

[B]     [B]*aπ [B]     [B,a=theta]θ

[from=theta, to=a,<',B]
[from=theta, to=b,<',B]

[]                           [a=a,B]*aπ [B]    [] [] [dd,3 vdots]

[B]     [B,a=theta](-1)^aθ

[a=b,B]*aπ [B]     []
[from=theta, to=a,<',B]
[from=theta, to=b,<',B]

[]  [o'] [rd,]          []

[a=myBase] [o.] [ru,]

[dr,-N.]     []                                          []

[ru,N'-] [rd,N.-]

[r,o'] [r,o.]

[]          []

Rules and theorems of the SZX calculus (the rules also hold when read from right to left and after exchanging colors, note that we omit the more generic Euler rule as it is not needed for the Clifford fragment that we use here). $a \in \{0,1\}^n$ and $b \in \{0,1\}^n$ are arbitrary vectors of binary variables, $\theta \in \R^n$ is an arbitrary vector, and operations between vectors are component-by-component. In the S rule, at least one connection must exist between both spiders, and bold wires indicate wires of size $\geq 1$.

The scalable ZX-calculus also provides a way to use arbitrary binary matrices to specify the connectivity between nodes: for any matrix $A \in \Z_2^{m \times n}$, we have:

\begin{align}
%% Definition of matrices
\left\llbracket\, \begin{ZX}
\zxN{} \rar[B] & [\zxwCol] \zxMatrix{A} \rar[B] &[\zxwCol] \zxN{}
\end{ZX} \,\right\rrbracket \eqSubeq[\coloneqq]{eq:defMatrix}{a} (\ket{x} \mapsto \ket{Ax})\qquad
\begin{ZX}[mbr]
\zxN{} \rar[B] & [\zxwCol] \zxMatrix{A} \rar[B] &[\zxwCol] \zxN{}
\end{ZX} \eqSubeq{eq:defMatrix}{b}
\begin{ZX}[mbr=2]
& [\zxwCol]                          & \zxZ{} \ar[dr] \ar[dd,3 vdots] &                                      & \zxX{} \ar[rd,'>] \ar[dd,3 vdots] &                          & [\zxwCol] \\
\zxN{} \rar[B,wc] & \zxDivider{} \ar[ru,<'] \ar[rd,<'] &                                & |[inner sep=.7mm]| A \ar[ru] \ar[rd] &                                   & \zxDivider-{} \rar[B,wc] & \zxN{}    \\
&                                    & [\zxwCol] \zxZ{} \ar[ru]       &                                      & \zxX{} \ar[ru,.>]                 &                                      \\
\end{ZX}\qquad
%% Definition of transposition
\begin{ZX}[mbr]
\zxN{} \rar[B] & \zxMatrix*{A} \rar[B] & \zxN{}
\end{ZX} \eqSubeq[\coloneqq]{eq:defMatrix}{c}
\begin{ZX}[mbr=2]
& [\zxWCol] \zxN{} \ar[B,dr,s]                 & [\zxWCol] \zxN{} \\[\zxZeroCol+.3mm]
\ar[B,dr,s] & \zxMatrix{A} \ar[B,u,C] \ar[B,d,C-] &                  \\
&                                              & \zxN{}           \\
\end{ZX}\label{eq:defMatrix}
\end{align}

Where, in the second equation, $A$ represents the biadjency matrix of the bipartite green/red graph.

For any binary vector $u$ and binary matrix $A$ and $B$ of appropriate size, we also have the following rewriting rules, that informally come from the fact that a green spider copies states in the computational basis while a red spider performs the modulo sum of its inputs:

[]                                                                    []

[B]     /_A
B [B,wc]      [ru,<',B] [rd,<.,B]

[]                               A [B]      []

[B]     [B] [ru,<',B] [rd,<.,B]

-B [B]

[B]     _A     B [B]
[]                                  A [rd,B,'>]                         []

[B,wc]      [ru,<',B] [rd,<.,B]                               [B] [B]

-B [ru,B,.>]

[B]     A + B [B]
[]                               A [rd,B,'>]                             []

[B,wc]     [B] [ru,<',B] [rd,<.,B]                               [B] [B]

-B [ru,B,.>]

[B]     BA [B]
[B]     [] A [B]     B [B]     []
[B,wc]    [] A [B]     [B]*uπ [B]    []
[B,wc]    [] [B]A^Tuπ [B]     A [B]    []
[B,wc]    [] A [B]     [BBw]*uπ
eq:matrixManipulationBc [mbr=1]
[B] [B,wc]    [] [BBw]A^Tuπ

[B,wc]    [] [B]*uπ [B]     A [B]    []
[B,wc]    [] A [B]     [B]Auπ [B]    []

[BBw]*uπ [B,wc]     A [B]    []
[BBw]Auπ [wc]    []

If $A$ is injective, we have
\zxN{} \rar[B] & \zxMatrix{A} \rar & \zxMatrix*{A} \rar[B] & \zxN{}
\end{ZX} =
\begin{ZX}[mbr=1,arrows={B}]
\zxNL \zxNR
\end{ZX}$
and similarly, if $A$ is surjective, we have
\zxN{} \rar[B] & \zxMatrix*{A} \rar & \zxMatrix{A} \rar[B] & \zxN{}
\end{ZX} =
\begin{ZX}[mbr=1,arrows={B}]
\zxNL \zxNR
\end{ZX}$. In particular, if $A$ is bijective, we have:

\begin{align}
\begin{ZX}[mbr=1,myBold]
\zxNL \zxMatrix{A} \zxNR
\end{ZX} \eqeqLem{lem:injectiveSurjective} \begin{ZX}[mbr=1,myBold]
\zxNL \zxMatrix{A} \rar & \zxMatrix{A^{-1}} \rar & \zxMatrix*{A^{-1}} \zxNR
\end{ZX} \eqSubeq{eq:matrixManipulationB}{a} \begin{ZX}[mbr=1,myBold]
\zxNL \zxMatrix{A^{-1}A} \rar & \zxMatrix*{A^{-1}} \zxNR
\end{ZX} = \begin{ZX}[mbr=1,myBold]
\zxNL \zxMatrix{I} \rar & \zxMatrix*{A^{-1}} \zxNR
\end{ZX} \eqSubeq{eq:defMatrix}{b} \begin{ZX}[mbr=1,myBold]
\zxNL \zxMatrix*{A^{-1}} \zxNR
\end{ZX}\label{eq:bijectionA}
\end{align}

§.§ Graph states
We list below some basic properties to graphically represent and manipulate graph states. Most of these facts and proofs can be found in <cit.>.

Let $\Gamma \in \Z_2^{m \times n}$, then the following ZX diagram applies a $\gateCZ$ between the $i$-th qubit of the first group of qubits and the $j$-th qubit of the second group of qubits iff $\Gamma_{j,i} = 1$, or, more formally:

\begin{align}
\begin{ZX}
\zxN{} \rar[Bn']   & [\zxWCol] \zxZ[B]{} \rar[Bn'] \dar[B] & [\zxWCol] \zxN{} \\
& \zxMatrix./{\Gamma} \dar[B,H={B}]     &                  \\[\zxHRow+1mm]
\zxN{} \rar[Bn'=m] & \zxZ[B]{} \rar[Bn'=m]                 & \zxN{}
\end{ZX}
= \prod_{(i,j), \Gamma_{j,i} = 1} \gateCZ_{i, m+j}
\end{align}

where $\gateCZ_{i, j}$ applies a $\gateCZ$ between the $i$-th and $j$-th qubit, assuming $i$, $j$ and the qubits are all indexed starting from $0$.

Let $G = (V, E)$ be an undirected graph on $n$ ordered vertices in $V$. By slightly abusing notations, we will also denote its representation in term of an adjacency matrix as $G \in \Z_2^{n \times n}$, the rows and columns of $G$ being indexed by elements in $V$, where $G_{i,j} = 1$ iff there exists an edge between $i$ and $j$ and $G_{i,j} = 0$ otherwise. We also denote $G^{\matrixUr}$ and $G^\matrixLl$ as, respectively, the upper and lower triangular matrix of $G$ (note that $G$ has zeros on its diagonal). In particular, $G = G^\matrixUr + G^\matrixLl$, and since $G^T = G$, we also have $(G^\matrixUr)^T = G^\matrixLl$. For any partition $(A,B)$ of $V$ of $G$ (for simplicity, we assume that elements in $V$ are ordered so that elements in $A$ appear before elements in $B$), we define $G_A \in \Z_2^{|A| \times |A|}$, $G_B \in \Z_2^{|B| \times |B|}$, and $\Gamma_{A \rightarrow  B} \in \Z_2^{|B| \times |A|}$ (or simply $\Gamma$) such that:

\begin{align}
G =
\begin{bmatrix}
G_A & \Gamma^T\\
\Gamma & G_B
\end{bmatrix}\label{eq:decompositionG}
\end{align}

In particular, $G_A$ and $G_B$ are the subgraphs of $G$ restricted to vertices in $A$ and $B$ respectively, and $\Gamma$ is the biadjency matrix between elements in $G_A$ and elements in $G_B$.

For any undirected graph $G = (V,E)$ on $n$ ordered vertices, we define $\zx[mbr]{\zxN{} \rar[Bn'] &[\zxWCol] \zxBox{G} \rar[Bn'] &[\zxWCol] \zxN{}}$ as the operation that applies a $\gateCZ$ gate between all input qubits connected in $G$ (the wires being ordered following the order on $V$). We can represent this operation diagrammatically (see <cit.>) as:

\begin{align}
\begin{aligned}
\begin{ZX}[myBold]
\zxN{} \rar[B] &[\zxwCol] \zxBox{G} \rar[B] &[\zxwCol]
\end{ZX} \eqdef
\begin{ZX}[myBold]
&                                       &                                                   &                                  & \\
& \zxH{} \ar[to=Gll,C'] \ar[to=root,<.] &                                                   & \zxMatrix[a=Gll]'/*{G^\matrixLl} & \\
\zxN{} \ar[rr] &                                       & [\zxwCol] \zxZ[a=root]{} \ar[B,rr] \ar[to=Gll,.>] &                                  &
\end{ZX}\label{eq:defGraphicalG}
\end{aligned}
\end{align}

Moreover, we define the graph states $G$ as $\zx{\zxBox{G} \rar[B] &[\zxwCol] \zxN{}} \eqdef \zx{\zxZ[B]{} \rar[B] &[\zxwCol] \zxBox{G} \rar[B] &[\zxwCol] \zxN{}}$.

For any graph $G$, $\left\llbracket\,\zx{\zxBox{G} \rar[B] &[\zxwCol]} \,\right\rrbracket = \ket{G}$.

The proof of this statement can be found in <cit.>, but the main idea is to show that this state is stabilized by the stabilizers of $\ket{G}$, which is formalized by the following lemma:

Let $G = (V,E)$ be a graph, and $x \in \Z_2^{|V|}$ be a vector (indexed by vertices in $V$). Then, $\zx{\zxNL \zxX[BBw]*{x\pi} \rar & \zxZ[BBw]{Gx\pi} \zxNR}$ is a stabilizer of $G$:

\begin{align}
\begin{ZX}
\zxBox{G} \rar & \zxX[BBw]*{x\pi} \rar & \zxZ[BBw]{Gx\pi} \zxNR
\end{ZX} =
\begin{ZX}[arrows={B}]
\zxBox{G} \zxNR
\end{ZX}\label{eq:stabilizerDiag}
\end{align}

The proof of this statement can be found in <cit.>, but we rewrite it here for completeness:

\begin{align}
\zxBox{G} \rar & \zxX[BBw]*{x\pi} \rar & \zxZ[BBw]{Gx\pi} \zxNR
\end{ZX} \eqeq{eq:defGraphicalG}
\begin{ZX}[myBold]
&                                                   &                                  & \\
\zxH{} \ar[to=Gll,C'] \ar[to=root,<.] &                                                   & \zxMatrix[a=Gll]'/*{G^\matrixLl} & \\
& [\zxwCol] \zxZ[a=root]{} \ar[B,rr] \ar[to=Gll,.>] &                                  & \zxX[BBw]*{x\pi} \rar & \zxZ[BBw]{Gx\pi} \zxNR
\end{ZX} \eqZX{Pi}
\begin{ZX}[myBold]
&                                               &                                       & \\
\zxH{} \dar \ar[to=Gll,C']       &                                               & \zxMatrix[a=Gll]'/*{G^\matrixLl} \dar & \\
\zxX[BBw]*{x\pi} \ar[to=root,<.] &                                               & \zxX[BBw]*{x\pi}                      & \\
& [\zxwCol] \zxZ[a=root]{} \ar[B,rr] \ar[ru,.>] &                                       & \zxZ[BBw]{Gx\pi} \zxNR
\end{ZX} \eqZXandSubeq{H}{eq:matrixManipulationC}{a}
\begin{ZX}[myBold]
&                                               &                             & \\
\zxZ[BBw]*{x\pi} \dar \ar[to=Gll,C'] &                                               & \zxX[BBw,a=Gll]*{G^\matrixLl x\pi} \dar & \\
\zxH{} \ar[to=root,<.]               &                                               & \zxMatrix[]'/*{G^\matrixLl} & \\
& [\zxwCol] \zxZ[a=root]{} \ar[B,rr] \ar[ru,.>] &                             & \zxZ[BBw]{Gx\pi} \zxNR
\end{ZX} \\&\eqZX{Pi}
\begin{ZX}[myBold]
&                                               &                             & \\
\zxX[BBw]*{G^\matrixLl x\pi} \dar \ar[to=Gll,C'] &                                               & \zxZ[BBw,a=Gll]*{x\pi} \dar & \\
\zxH{} \ar[to=root,<.]                           &                                               & \zxMatrix[]'/*{G^\matrixLl} & \\
& [\zxwCol] \zxZ[a=root]{} \ar[B,rr] \ar[ru,.>] &                             & \zxZ[BBw]{Gx\pi} \zxNR
\end{ZX} \eqZXandSubeq{H}{eq:matrixManipulationB}{b}
\begin{ZX}[myBold]
&                                                   &                                       & \\
\zxH{} \dar \ar[to=Gll,C']                        &                                                   & \zxMatrix[a=Gll]'/*{G^\matrixLl} \dar & \\
\zxZ[BBw]*{G^\matrixLl x\pi} \ar[wcs, to=root,<.] &                                                   & \zxZ[BBw]*{G^\matrixLl x\pi}          & \\
& [\zxwCol] \zxZ[a=root]{} \ar[B,rr] \ar[ru,wce,.>] &                                       & \zxZ[BBw]{Gx\pi} \zxNR
\end{ZX} \eqZX{S}
\begin{ZX}[myBold]
&                                                   &                                  & \\
\zxH{} \ar[to=Gll,C'] \ar[wcs, to=root,<.] &                                                   & \zxMatrix[a=Gll]'/*{G^\matrixLl} & \\
& [\zxwCol] \zxZ[a=root]{} \ar[B,rr] \ar[ru,.>,wce] &                                  & \zxZ[BBw]{(Gx \xor Gx)\pi} \zxNR
\end{ZX} \eqZX{I}
\begin{ZX}[myBold]
\zxBox{G} \zxNR
\end{ZX}
\end{align}

For any graph $G$, $
\begin{ZX}[mbr=1]
\rar[B] &[\zxwCol] \zxBox{G} \rar[B] & \zxBox{G} \rar[B] &[\zxwCol]
\end{ZX}  =
\begin{ZX}[mbr=1]
\rar[B] &[\zxWCol]
\end{ZX}

This fact is a direct consequence of the property $\gateCZ\gateCZ = \gateI$. More formally:

\begin{align}
\begin{ZX}[mbr=1]
\rar[B] &[\zxwCol] \zxBox{G} \rar[B] & \zxBox{G} \rar[B] &[\zxwCol]
\end{ZX} &\eqeqDef{def:graphDiag}
\begin{ZX}[myBold,mbr=1]
& \zxH{} \ar[to=Gll,C'] \ar[to=root,<.] &                                                    & \zxMatrix[a=Gll]'*{G^\matrixLl} & \zxH{} \ar[to=Gll2,C'] \ar[to=root2,<.] &                                                     & \zxMatrix[a=Gll2]'*{G^\matrixLl} & \\
\zxN{} \ar[rr] &                                       & [\zxwCol] \zxZ[a=root]{} \ar[B,rrr] \ar[to=Gll,.>] &                                 &                                         & [\zxwCol] \zxZ[a=root2]{} \ar[B,rr] \ar[to=Gll2,.>] &                                   &
\end{ZX} \eqZX{S}
\begin{ZX}[myBold,mbr=1]
& \zxH{} \ar[to=Gll,C'] \ar[to=root,<.] & \zxH{} \ar[to=Gll2,C'] \ar[to=root]      & \zxMatrix[a=Gll2].*{G^\matrixLl} \ar[to=root2,<.] &                                                                  & \zxMatrix[a=Gll]'*{G^\matrixLl} \\
\zxN{} \ar[rr] &                                       & [\zxwCol] \zxZ[a=root]{} \ar[B,to=root2] &                                  & [\zxwCol] \zxZ[a=root2]{} \ar[B,rr] \ar[to=Gll,.>]   &  &
\end{ZX} \eqZX{H}
\begin{ZX}[myBold,mbr=2]
& [\zxwCol]   & [\zxWCol+1mm]                                                 & \zxMatrix[a=Gll]*{G^\matrixLl}                   &                                                    & [\zxWCol] \\
&             &                                                               & \zxMatrix[a=Gll2]*{G^\matrixLl} \ar[to=root2,C-] &                                                    &           \\
\zxN{} \rar[] & \zxH{} \rar & \zxX[a=root]{} \ar[to=Gll2,C] \ar[to=Gll,C] \ar[B,to=root2,H] &                                                  & [\zxwCol] \zxZ[a=root2]{} \ar[B,rr] \ar[to=Gll,C-] &  &
\end{ZX}\\ &\eqSubeq{eq:matrixManipulationA}{c}
\begin{ZX}[myBold,mbr=3]
&                                                                                \\
& [\zxwCol]   & [\zxwCol]                                      & \zxMatrix[a=Gll]/*{G^\matrixLl+G^\matrixLl} &                                                    & [\zxWCol] \\
\zxN{} \rar[] & \zxH{} \rar & \zxX[a=root]{} \ar[to=Gll,C] \ar[B,to=root2,H] &                                             & [\zxwCol] \zxZ[a=root2]{} \ar[B,rr] \ar[to=Gll,C-] &  &
\end{ZX} =
\begin{ZX}[myBold,mbr=3]
&                                                                                \\[2mm]
& [\zxwCol]   & [\zxwCol]                                      & \zxMatrix[a=Gll]/*{0} &                                                    & [\zxWCol] \\
\zxN{} \rar[] & \zxH{} \rar & \zxX[a=root]{} \ar[to=Gll,C] \ar[B,to=root2,H] &                       & [\zxwCol] \zxZ[a=root2]{} \ar[B,rr] \ar[to=Gll,C-] &  &
\end{ZX} \eqSubeq{eq:defMatrix}{b}
\begin{ZX}[myBold,mbr=3]
&                                                                                \\
& [\zxwCol]   & [\zxwCol]      \zxX[a=Glle]{}      &             & \zxZ[a=Glls]{}                                      & [\zxWCol] \\
\zxN{} \rar[] & \zxH{} \rar & \zxX[a=root]{} \ar[to=Glle,C] \rar & \zxH{} \rar & [\zxwCol] \zxZ[a=root2]{} \ar[B,rr] \ar[to=Glls,C-] &  &
\end{ZX} \eqZXXX{H}{S}{I}
\begin{ZX}[myBold]
\zxN{} \rar &[\zxWCol] \zxN{}
\end{ZX}
\end{align}

For any graph $G$, $
\begin{ZX}[mbr=2]
& [\zxwCol] \dar   & [\zxwCol]         & [\zxwCol] \\
\rar & \zxZ[BBw]{} \rar & \zxBox{G} \rar[B] &
\end{ZX}  =
\begin{ZX}[mbr=2]
& [\zxwCol]      & [\zxwCol] \dar & [\zxwCol] \\
\rar[B] & \zxBox{G} \rar & \zxZ[BBw]{} \rar    &
\end{ZX}

This is a direct application of the spider rule on the definition of [myBold]G .

We describe now a way to partition a graph $G$ into two subgraphs.

Let $G = (V,E)$. Let $H \subseteq V$ and $M \eqdef V \setminus H$ be a partition of $V$ (for simplicity we assume that we re-order elements in $V$ so that elements in $H$ are smaller than elements in $M$). Then, using notations from <ref>, we have:

\begin{align}
\zx[mbr=2,myBold]{
& [\zxwCol]                          & [\zxwCol] \\
\zxBox{G} \rar[B] & \zxDivider{} \ar[ru,<'] \ar[rd,<.] &           \\
&                                    &
\begin{ZX}[myBold]
\zxBox{G_H} \rar[B] & [\zxWCol] \zxZ{} \rar[B] \dar[B]                      & [\zxWCol] \zxN{} \\
& \zxMatrix./{\Gamma^G_{H \rightarrow M}} \dar[B,H={B}] &                  \\[\zxHRow+1mm]
\zxBox{G_M} \rar[B] & \zxZ{} \rar[B]                                        & \zxN{}
\end{ZX}
\end{align}

Intuitively, this lemma only means that in order to create $G$, we can first create the graph states $G_H$ and $G_M$, and apply after $\gateCZ$ gates between elements in $G_H$ and $G_M$. This can be formalized diagrammatically using the decomposition rules for block matrices:

\begin{align}
\ket{G} &\eqeqDef{def:graphDiag}
\begin{ZX}[myBold,mbr=2]
\zxH{} \ar[to=Gll,C'] \ar[to=root,<.] &                                                   & \zxMatrix[a=Gll]'/*{G^\matrixLl} &                                                & \\
& [\zxwCol] \zxZ[a=root]{} \ar[B,rr] \ar[to=Gll,.>] &                                 & \zxDivider[a=finalDiv]{} \ar[ru,<'] \ar[rd,<.] & \\[\zxwRow]
&                                                   &                                 &                                                &
\end{ZX} \eqeq{eq:decompositionG}
\begin{ZX}[myBold,mbr=2]
\zxH{} \ar[to=Gll,C'] \ar[to=root,<.] &                                                   & \zxMatrix[a=Gll]'*_{G_H^\matrixLl & 0 \\\Gamma & G_M^\matrixLl}{} &                                                &[\zxwCol] \\
& [\zxwCol] \zxZ[a=root]{} \ar[B,rr] \ar[to=Gll,.>] &                                                             & \zxDivider[a=finalDiv]{} \ar[ru,<'] \ar[rd,<.] &           \\[\zxwRow]
&                                                   &                                                             &                                                &
\end{ZX} \eqSubeq{eq:matrixManipulationA}{a}
\begin{ZX}[myBold,mbr=3]
& \zxDivider[a=div]{} \ar[to=Gll,'>]  \ar[to=Gll2,'>={1-=1,1L=0,2-=0}]                         &                                   &                                                                               \\
\zxH{} \ar[to=div,<',wce] \ar[to=root,<.] &                                                                                & \zxMatrix[a=Gll]'*_{G_H^\matrixLl & 0}{} & \zxMatrix[a=Gll2]'*_{\Gamma                    & G_M^\matrixLl}{} &  &[\zxwCol] \\
& [\zxwCol] \zxZ[a=root]{} \ar[B,to=finalDiv] \ar[to=Gll,.>] \ar[to=Gll2,.>={1-=.8,1L=0,2-=0}] &                                   &      & \zxDivider[a=finalDiv]{} \ar[ru,<'] \ar[rd,<.] &                  &  & \\[\zxwRow]
&                                                                                &                                   &      &                                                &
\end{ZX} \\&\eqSubeq{eq:matrixManipulationA}{b}
\begin{ZX}[myBold,mbr=3]
& \zxDivider[a=div]{} \ar[to=gatherA,'>]  \ar[to=gatherB,'>={1-=1,1L=0,2-=0}]           &                                                                      &                        &                                                                                \\
&                                                                                & \zxX[a=gatherA]{} \ar[to=Gll] \ar['>={1-=.8,1L=0,2-=0},to=zero]      &                        & \zxX[a=gatherB]{}  \ar[to=Gll2] \ar[to=GM,'>={1-=.8,1L=0,2-=0}]                                                        \\
\zxH{} \ar[to=div,<',wce] \ar[to=root,<.] &                                                                                & \zxMatrix[a=Gll]'*{G_H^\matrixLl}                                    & \zxMatrix[a=zero]'*{0} & \zxMatrix[a=Gll2]'*{\Gamma}                                         & \zxMatrix[a=GM]'*{G_M^\matrixLl}                 \\
&                                                                                & \zxDivider[a=dividA]{} \ar[to=Gll] \ar[to=zero,.>={1-=.8,1L=0,2-=0}] &                        & \zxDivider[a=dividB]{} \ar[to=Gll2] \ar[to=GM,.>={1-=.8,1L=0,2-=0}] &                                                & \\
& [\zxwCol] \zxZ[a=root]{} \ar[B,to=finalDiv] \ar[to=dividA,S,wce] \ar[to=dividB,s,wce] &                                                                      &                        &                                                                     & \zxDivider[a=finalDiv]{} \ar[ru,<'] \ar[rd,<.] & \\[\zxwRow]
&                                                                                &                                                                      &                        &                                                                     &                                                &  &  &
\end{ZX} \eqSubeq{eq:defMatrix}{b}
\begin{ZX}[myBold,mbr=3]
& \zxDivider[a=div]{} \ar[to=Gll,'>]  \ar[to=gatherB,'>={1-=1,1L=0,2-=0}]               &                                                                      &                &                                                                                \\
&                                                                                &                                                                      &                & \zxX[a=gatherB]{}  \ar[to=Gll2] \ar[to=GM,'>={1-=.8,1L=0,2-=0}]                                                        \\
\zxH{} \ar[to=div,<',wce] \ar[to=root,<.] &                                                                                & \zxMatrix[a=Gll]'*{G_H^\matrixLl}                                    & \zxZ[a=zero]{} & \zxMatrix[a=Gll2]'*{\Gamma}                                         & \zxMatrix[a=GM]'*{G_M^\matrixLl}                 \\
&                                                                                & \zxDivider[a=dividA]{} \ar[to=Gll] \ar[to=zero,.>={1-=.8,1L=0,2-=0}] &                & \zxDivider[a=dividB]{} \ar[to=Gll2] \ar[to=GM,.>={1-=.8,1L=0,2-=0}] &                                                & \\
& [\zxwCol] \zxZ[a=root]{} \ar[B,to=finalDiv] \ar[to=dividA,S,wce] \ar[to=dividB,s,wce] &                                                                      &                &                                                                     & \zxDivider[a=finalDiv]{} \ar[ru,<'] \ar[rd,<.] & \\[\zxwRow]
&                                                                                &                                                                      &                &                                                                     &                                                &  &  &
\end{ZX} \\&\eqZXXX{Z}{W}{R}
\begin{ZX}[myBold]
&                                                                    &                                                                                &  &                               \\
&                                                                    &                                                                                &  &                               \\
\zxH{} \ar[to=Gll,C']  \ar[to=root,<.] &                                                                    & \zxMatrix[a=Gll]'*{G_H^\matrixLl}                                                              &  &  &                            \\
&                                                                    &                                                                                &  &  &                &           \\
& [\zxwCol] \zxZ[a=root]{} \ar[to=end1]  \ar[to=Gll,.>] \ar[to=Gll2,'>] &                                                                                &  &  & \zxN[a=end1]{} &           \\[\zxwRow]
&                                                                    & \zxMatrix[a=Gll2]'{\Gamma}                                                                                \\
&                                                                    & \zxX[a=gatherB]{}  \ar[to=Gll2] \ar[to=GM,'>={1-=.8,1L=0,2-=0}]                                                                   \\
&                                                                    & \zxH{} \ar[to=root2] \ar[to=gatherB]                                                           & \zxMatrix[a=GM]'*{G_M^\matrixLl} \\
& \zxZ[a=zero]{}                                                     & \zxZ[a=root2]{} \ar[to=zero,.>={1-=.8,1L=0,2-=0}] \ar[to=end2] \ar[to=GM,.>={1-=.8,1L=0,2-=0}] &  &  & \zxN[a=end2]{} &  &  &
\end{ZX} \eqZXX{S}{H}
\begin{ZX}[myBold]
\zxBox{G_H} \rar[B] & [\zxWCol] \zxZ{} \rar[B] \dar[B]                      & [\zxWCol] \zxN{} \\
& \zxMatrix./{\Gamma} \dar[B,H={B}] &                  \\[\zxHRow+1mm]
\zxBox{G_M} \rar[B] & \zxZ{} \rar[B]                                        & \zxN{}
\end{ZX}
\end{align}

Let $\Gamma \in \Z_2^{m \times n}$ be a binary matrix. Then, there exists an invertible matrix $U \in \Z_2^{n \times n}$, an integer $r$ (the rank), a matrix $R \in \Z_2^{r \times n-r}$ and an invertible matrix $V \in \Z_2^{m \times m}$ such that:

\begin{align}
\Gamma = V
\begin{bmatrix}
I_r & R\\
\mathbf{0} & \mathbf{0}
\end{bmatrix}
\end{align}

where $I_r \in \Z_2^{r \times r}$ is the identity matrix and $\mathbf{0}$ is the zero matrix.

This is a direct consequence of the Gaussian elimination algorithm: using Gaussian elimination we can obtain a row echelon form (using only elementary row operations, i.e. swapping rows and adding a multiple of one row to another row). Then using column swap, we can reorder the row echelon form matrix to bring the pivots on the diagonal of the matrix. Finally, by subtracting for each row $j$ (starting from the last row) the rows $i$ (for any $i > j$) if $j$'s row contains a one on $i$-th column, we can remove all elements above the diagonal, leading to the identity in the upper right corner. By combining all (invertible) elementary row and column operations into $U$ and $V$, we obtain our final form.

Let $U \in \Z_2^{n \times n}$ be an invertible matrix, then $\zx[mbr,arrows={B}]{\rar &[\zxwCol] \zxMatrix{U} \rar &[\zxwCol]}$ is physically implementable without auxiliary qubits using only $\gateCNOT$ and swap operations, and $\zx[mbr,arrows={B}]{\rar &[\zxwCol] \zxMatrix*{U} \rar &[\zxwCol]} = \zx[mbr,arrows={B}]{\rar &[\zxwCol] \zxMatrix{U^{-1}} \rar &[\zxwCol]}$ .

The fact that $\zx[mbr,arrows={B}]{\rar &[\zxwCol] \zxMatrix*{U} \rar &[\zxwCol]} = \zx[mbr,arrows={B}]{\rar &[\zxwCol] \zxMatrix{U^{-1}} \rar &[\zxwCol]}$ is a direct consequence of <cit.>. To see that it can be written as a sequence of  and swap operations, we can first realize that since $U$ is invertible, using the Gaussian elimination, we can find elementary row and column operations $E_1, \dots, E_n$ and $E'_1, \dots, \times E'_n$ such that:

\begin{align}
E_1  \dots  E_n U E'_1  \dots  E'_n = I
\end{align}

The elementary row (resp. column) operations can either be:

* Operation 1: Multiply line (resp. column) $j$ by a non-null scalar: since the only non-null scalar modulo $2$ is $1$, all operations of this form would be identity so we can remove such operations.

* Operation 2: Exchange the $j$-th line (resp. column) and the $j'$-th line (resp. column).

* Operation 3: Add the column $j$ to column $j'$ (in theory, we can multiply first the $j$-th line by an arbitrary factor, but since we are working modulo $2$, the only interesting case is when this scalar is $1$ since when it is equal to $0$ nothing happens)

We can see that all these operations are self-inverse, so we have:

\begin{align}
U = E_n  \dots  E_1 E'_n  \dots  E'_1
\end{align}

\begin{align}
\zx[myBold,mbr=1]{\zxNL \zxMatrix{U} \zxNR} = \zx[myBold,mbr=1]{\zxNL \zxMatrix{E'_1} \rar & \dots \rar & \zxMatrix{E'_n} \rar & \zxMatrix{E_1} \rar & \dots \rar & \zxMatrix{E_n} \zxNR}
\end{align}

Moreover, any such operation can be implemented using a swap or a  gate. If the elementary operation $E$ is Operation 2, i.e. a swap, then $E$ can literally be implemented by the same swap operation. This can be seen for instance by realizing that a swap can be realized via a matrix of this form:

\begin{align}
E = \begin{bmatrix}
\mathbf{1^k}        \\
& 0 &  & 1         \\
&   & \mathbf{1^l} \\
& 1 &  & 0         \\
&   &  &  & \mathbf{1^m}
\end{bmatrix}\label{eg:diagSwap}
\end{align}

where $1^k$ is the diagonal matrix of size $k \times k$ with ones on its diagonal, and $k=j-1$, $l=j'-j-1$. Therefore, using the characterization in <ref>, we have:

\begin{align}
\begin{ZX}[myBold,mbr=1]
\zxNL \zxMatrix{E} \zxNR
\end{ZX} \eqSubeq{eq:defMatrix}{b}
\begin{ZX}[mbr=2]
& [\zxwCol]                          & \zxZ{} \ar[dr] \ar[dd,3 vdots] &                                      & \zxX{} \ar[rd,'>] \ar[dd,3 vdots] &                          & [\zxwCol] \\
\zxN{} \rar[B,wc] & \zxDivider{} \ar[ru,<'] \ar[rd,<'] &                                & |[inner sep=.7mm]| E \ar[ru] \ar[rd] &                                   & \zxDivider-{} \rar[B,wc] & \zxN{}    \\
&                                    & [\zxwCol] \zxZ{} \ar[ru]       &                                      & \zxX{} \ar[ru,.>]                 &
\end{ZX} \eqeq{eg:diagSwap}
\begin{ZX}[mbr=3]
\rar[Bn'Args={k}{}]       & [\zxWCol] \zxZ[B]{} \rar[B] & [\zxWCol+3mm] \zxX[B]{} \rar[B] & [\zxWCol] \\[.5mm]
\zxN{} \rar               & \zxZ{} \ar[to=jprime,S]     & \zxX[a=j]{}      \rar           &           \\[.5mm]
\rar[Bn'Args={l}{pos=.2}] & \zxZ[B]{} \rar[B]           & \zxX[B]{} \rar[B]               &           \\[.5mm]
\zxN{} \rar               & \zxZ{} \ar[to=j,S]          & \zxX[a=jprime]{} \rar           &           \\[.5mm]
\rar[Bn.Args={m}{}]       & \zxZ[B]{} \rar[B]           & \zxX[B]{} \rar[B]               &
\end{ZX} \eqZX{I}
\begin{ZX}[mbr=3]
\rar[Bn'Args={k}{}]       & [\zxWCol+5mm]    \\[.5mm]
\zxN{} \ar[to=jprime,S]   & \zxN[a=j]{}      \\[.5mm]
\rar[Bn'Args={l}{pos=.2}] &                  \\[.5mm]
\zxN{} \ar[to=j,S]        & \zxN[a=jprime]{} \\[.5mm]
\rar[Bn.Args={m}{}]       &
\end{ZX}
\end{align}

Similarly, if $E$ is Operation 3, then we can write $E$ as a matrix of this form (the $1$ might be on the other side of the diagonal if $j' < j$):

\begin{align}
E = \begin{bmatrix}
\mathbf{1^k} \\
& 1 &  &             \\
&   & \mathbf{1^l}    \\
& 1  &  & 1            \\
&   &  &  & \mathbf{1^m}
\end{bmatrix}\label{eg:formCNOT}
\end{align}

where $k=j-1$, $l=j'-j-1$ which gives, using the characterization in <ref>:

\begin{align}
\begin{ZX}[myBold,mbr=1]
\zxNL \zxMatrix{E} \zxNR
\end{ZX} \eqSubeq{eq:defMatrix}{b}
\begin{ZX}[mbr=2]
& [\zxwCol]                          & \zxZ{} \ar[dr] \ar[dd,3 vdots] &                                      & \zxX{} \ar[rd,'>] \ar[dd,3 vdots] &                          & [\zxwCol] \\
\zxN{} \rar[B,wc] & \zxDivider{} \ar[ru,<'] \ar[rd,<'] &                                & |[inner sep=.7mm]| E \ar[ru] \ar[rd] &                                   & \zxDivider-{} \rar[B,wc] & \zxN{}    \\
&                                    & [\zxwCol] \zxZ{} \ar[ru]       &                                      & \zxX{} \ar[ru,.>]                 &
\end{ZX} \eqeq{eg:formCNOT}
\begin{ZX}[mbr=3]
\rar[Bn'Args={k}{}]       & [\zxWCol] \zxZ[B]{} \rar[B]  & [\zxWCol+3mm] \zxX[B]{} \rar[B] & [\zxWCol] \\[.5mm]
\zxN{} \rar               & \zxZ{} \rar \ar[to=jprime,S] & \zxX[a=j]{}      \rar           &           \\[.5mm]
\rar[Bn'Args={l}{pos=.2}] & \zxZ[B]{} \rar[B]            & \zxX[B]{} \rar[B]               &           \\[.5mm]
\zxN{} \rar               & \zxZ{} \rar                  & \zxX[a=jprime]{} \rar           &           \\[.5mm]
\rar[Bn.Args={m}{}]       & \zxZ[B]{} \rar[B]            & \zxX[B]{} \rar[B]               &
\end{ZX} \eqZX{I}
\begin{ZX}[mbr=3]
\rar[B]     & [\zxWCol] \zxN{} \rar[B]   &[\zxWCol] \\[.5mm]
\zxN{} \rar & \zxZ{} \rar \ar[to=jprime] &          \\[.5mm]
\rar[B]     & \zxN{} \rar[B]             &          \\[.5mm]
\zxN{} \rar & \zxX[a=jprime]{} \rar      &          \\[.5mm]
\rar[B]     & \zxN{} \rar[B]             &
\end{ZX}
\end{align}

which corresponds exactly to a  gate where the $j$-th qubit is the source and the $j'$-th qubit is the target.

§ PROOFS

We details in this appendix some proofs of the main paper.