Finite authenticated key-distribution protocol

Fix finite nonempty sets $\mathsf{K}$ and $\mathsf{T}$ of key values and public transcripts, respectively, and fix an ordering of each finite set. Choose a symbol $\mathrm{\perp }\mathrm{\notin }\mathsf{K}$ and order $\mathsf{K}\cup \{\mathrm{\perp }\}$ by placing $\mathrm{\perp }$ after the ordered keys. The full key registers $A$ and $B$ are copies of $Q_{\mathrm{\mid }\mathsf{K}\mathrm{\mid }+1}$, with computational basis labelled by $\mathsf{K}\cup \{\mathrm{\perp }\}$; the transcript register $T$ is $Q_{\mathrm{\mid }\mathsf{T}\mathrm{\mid }}$, with basis labelled by $\mathsf{T}$, using Finite registers and their ordered computational bases. For accepted-state calculations, identify the subspaces spanned by the key vectors $\mathrm{\mid }a⟩$, $a\in \mathsf{K}$, with $Q_{\mathrm{\mid }\mathsf{K}\mathrm{\mid }}$; operators on these subspaces are embedded in the full key registers by zero extension. A finite two-party key-distribution protocol is a finite-round interaction of Alice and Bob in which each quantum register is nonzero and finite-dimensional, every local quantum operation is a quantum channel or finite instrument (Finite-dimensional quantum channel, Finite instruments and conditional states), and every classical message alphabet is finite. Eve's operation on each insecure quantum transmission is a channel from the sent register and her current memory to the received register and her updated memory. The parties communicate through an ideal authenticated public channel: each message is delivered unchanged to its intended honest recipient, and Eve receives a copy. The transcript $t\in \mathsf{T}$ records all such messages, including messages that lead the protocol to abort. This is an assumption about the communication resource; it does not prove security of an authentication implementation. Any implementation error must be included in the abort convention or in an additional security parameter.

For each allowed adversarial strategy, the final output is a normalized state, classical in the key registers $A,B$ and transcript register $T$, on $A\otimes B\otimes T\otimes E$, where $E$ is Eve's retained finite-dimensional quantum system. Both honest parties output the common abort symbol $\mathrm{\perp }$ on an abort. In the ordered product basis this state has the form

${\rho }_{ABTE}={\sum }_{t\in \mathsf{T}}\mathrm{\mid }\mathrm{\perp },\mathrm{\perp },t⟩⟨\mathrm{\perp },\mathrm{\perp },t\mathrm{\mid }\otimes {\omega }_E^{\mathrm{\perp },t}+{\sum }_{a,b\in \mathsf{K},t\in \mathsf{T}}\mathrm{\mid }a,b,t⟩⟨a,b,t\mathrm{\mid }\otimes {\omega }_E^{a,b,t},$

where every block ${\omega }_E^{\mathrm{\perp },t}$ and ${\omega }_E^{a,b,t}$ is nonnegative and the sum of their traces is $1$. The trace of each block is the joint probability of its displayed classical labels. All registers and tensor factors retain the displayed order. The transcript is included separately from $E$ so that secrecy below explicitly conditions on the public messages as well as Eve's quantum information.