1: \documentclass{entcs} \usepackage{prentcsmacro}

2: 

3: 

4: \usepackage{amsmath, amssymb, stmaryrd, wasysym, xspace}

5: \usepackage{graphicx}

6: 

7: 

8: 

9: %%% geprutst in bbl file bij Halpern95 - anders wou boektitel niet showen

10: %%% in prentcsmacro stuk uitgecomment omdat ik foutmeldingen kreeg. 

11: 

12: \def\mat#1{\ensuremath{#1}\xspace}

13: 

14: 

15: 

16: 

17: %%Environments%%

18: \def\AR#1{\begin{align}#1\end{align}}

19: \def\ARA#1{\begin{alignat}{2}#1\end{alignat}}

20: \def\SP#1{\begin{split}#1\end{split}}

21: \def\GA#1{\begin{gather}#1\end{gather}}

22: \def\MA#1{\left(\begin{matrix}#1\end{matrix}\right)}

23: \def\CA#1{\begin{cases}#1\end{cases}}

24: \def\EQ#1{\begin{equation}#1\end{equation}}

25: \def\se#1{Sec.~\ref{#1}}

26: \def\ses#1#2{Secs.~\ref{#1} and \ref{#2}}

27: \def\de#1{Def.~\ref{#1}}

28: \def\defs#1#2{Defs.~\ref{#1} and \ref{#2}}

29: \def\pro#1{Prop.~\ref{#1}}

30: \def\pros#1#2{Props.~\ref{#1} and \ref{#2}}

31: \def\eq#1{Eq.\eqref{#1}}

32: \def\eqs#1#2{Eqs.\eqref{#1} and \eqref{#2}}

33: \def\fig#1{Fig.~\ref{#1}}

34: \def\figs#1#2{Figs.~\ref{#1} and \ref{#2}}

35: \def\proof{\tbf{Proof. }}

36: \def\ens#1{\{#1\}}

37: \def\tc#1{\textcolor{redex}{#1}}

38: \def\tb#1{\textcolor{blue}{#1}}

39: 

40: 

41: %%Quantum Stuff%%

42: 

43: \newcommand{\ket}[1]{\mbox{$|#1\rangle$}}

44: \newcommand{\gket}{\ket{\psi}}

45: \newcommand{\0}{\ket{0}}

46: \newcommand{\1}{\ket{1}}

47: \newcommand{\zz}{\ket{00}}

48: \newcommand{\zo}{\ket{01}}

49: \newcommand{\oz}{\ket{10}}

50: \newcommand{\oo}{\ket{11}}

51: \newcommand{\bra}[1]{\mbox{$\langle#1|$}}

52: \newcommand{\ketbra}[2]{\mbox{$|#1\rangle\langle#2|$}}

53: \newcommand{\braket}[2]{\mbox{$\langle#1|#2\rangle$}}

54: \newcommand{\proj}[1]{\ketbra{#1}{#1}}

55: \newcommand{\pc}{\ket{0}+\ket{1}}

56: \newcommand{\mc}{\ket{0}-\ket{1}}

57: \newcommand{\p}{\ket{+}}

58: \newcommand{\m}{\ket{-}}

59: \newcommand{\ebit}{\ket{00}+\ket{11}}

60: \newcommand{\ebzo}{\ket{01}-\ket{10}}

61: \newcommand{\eboz}{\ket{01}+\ket{10}}

62: \newcommand{\eboo}{\ket{00}-\ket{11}}

63: \def\bell#1{\ket{\Phi_{#1}}}

64: \def\ztwo#1{\mbb Z_{2}^{#1}}  

65: \def\ctwo#1{(\mbb C^2)^{\ox#1}}  

66: 

67: \newcommand{\tr}[1]{\ensuremath{\mathrm{Tr}(#1)}}

68: \newcommand{\Tr}[1]{\ensuremath{\mathbf{tr}(#1)}}

69: \newcommand{\eff}[1]{\ensuremath{\cE(#1)}}

70: \newcommand{\treq}{\trianglelefteqslant}

71: \newcommand{\norm}{\cN orm(\cH)}

72: \newcommand{\dm}{\cD \cM(\cH)}

73: \def\den#1{\cD({#1})}

74: \newcommand{\herm}{\cH erm(\cH)}

75: \newcommand{\pred}{\cP(\cH)}

76: \newcommand{\prtf}{\cP\cT(\cH)}

77: \newcommand{\cp}{\cC\cP(\cH)}

78: \newcommand{\wpr}[1]{\mbox{$\mathrm{wp}(#1)$}}

79: \newcommand{\lowner}{L\"{o}wner}

80: \newcommand{\veq}[1]{\stackrel{\rm{#1}}{=}}

81: \newcommand{\lub}[1]{\sqcup_{#1}}

82: \newcommand{\perm}{\mathrm{Perm}}

83: 

84: \newcommand{\locc}{\equiv_{LOCC}}

85: \newcommand{\lu}{\equiv_{LU}}

86: \newcommand{\slocc}{\equiv_{SLOCC}}

87: 

88: \def\qc{QC_{\cC}}

89: \def\wq{1WQC\xspace}

90: \def\tq{TQC\xspace}

91: \def\mtc{M$^{2}$C \xspace}

92: \def\MS#1#2#3#4{{}^{#4}[{M}_{#2}^{#1}]^{#3}}

93: \def\ms#1#2#3{\MS{#1}{#2}{#3}{}}

94: \def\Ms#1#2{{M}_{#2}^{#1}}

95: \def\M#1#2{{M}_{#2}^{#1}}

96: \def\tM#1#2#3#4{M_{#3#4}^{#1,#2}}

97: \def\TMR#1#2#3#4#5#6{[{M}_{#3#4}^{#1,#2}]^{(#5,#6)}}

98: \def\a#1#2{{}^{#2}[\al ]^{#1}}

99: \def\as#1{\a#1{}}

100: \def\at#1{\a{}#1}

101: \def\cz#1#2{Z_{#1}^{#2}}

102: \def\cx#1#2{X_{#1}^{#2}}

103: \def\Cz#1{Z_{#1}}

104: \def\Cx#1{X_{#1}}

105: \def\et#1#2{E_{#1#2}}

106: \def\sss#1#2{S_{#1}^{#2}}

107: \def\pp#1{\langle +_{#1}|_i \;}

108: \def\mp#1{\langle -_{#1}|_i \;}

109: \def\nor#1{\|#1\|}

110: \def\ost{\frac1{\sqrt2}}

111: \def\most{\frac{-1}{\sqrt2}}

112: \def\ctR{\mathop{\wedge}\hskip-.4ex}

113: 

114: \def\nr{ \;|\; }

115: \def\given{\, \| \,}

116: \def\qc{\mathtt{qc}} 

117: \def\cc{\mathtt{c}} 

118: \def\qci{\mathtt{qc?}} 

119: \def\cci{\mathtt{c?}} 

120: \def\qco{\mathtt{qc!}} 

121: \def\cco{\mathtt{c!}} 

122: \def\qcio{\mathtt{qc!?}} 

123: \def\ccio{\mathtt{c!?}} 

124: \def\init#1{\mrm{init(}#1\mrm{)}}

125: \def\fin#1{\mrm{fin(}#1\mrm{)}}

126: 

127: %%Symbols%%

128: \def\rar{\rightarrow}

129: \def\xrar{\xrightarrow}

130: \def\hrar{\hookrightarrow}

131: \def\lrar{\longrightarrow}

132: \def\Rar{\Rightarrow}

133: \def\Lrar{\Longrightarrow}

134: \def\lar{\leftarrow}

135: \def\Lar{\Leftarrow}

136: \def\xlar{\xleftarrow}

137: \def\dar{\downarrow}

138: \def\lra{\rightleftarrows}

139: \def\slar#1{\stackrel{#1}{\lrar}}

140: \def\Slar#1{\stackrel{#1}{\Lrar}}

141: \def\ovs{\overset}

142: \def\st{^\star}

143: \newcommand{\x}{\times}

144: \newcommand{\os}{\oslash}

145: \newcommand{\oa}{\oplus}

146: \newcommand{\ox}{\otimes}

147: \newcommand{\bigox}{\bigotimes}

148: \newcommand{\bigoa}{\bigoplus}

149: \newcommand{\ent}{\vdash}

150: \newcommand{\Ent}{\vDash}

151: \newcommand{\imp}{\Rightarrow}

152: \newcommand{\cont}{\subseteq}

153: \newcommand{\comp}{\mathbb{C}}

154: \newcommand{\reals}{\mathbb{R}}

155: \newcommand{\nats}{\mathbb{N}}

156: \def\qed{\ensuremath{\Box}}

157: \def\emptyset{\varnothing}

158: \def\bs{\backslash}

159: \def\t{~}

160: \def\pre{\triangleleft}

161: \def\alw{\Box}

162: \def\eve{\Diamond}

163: \def\nex{\fullmoon}

164: 

165: \newcommand{\semantics}[1]{[\![ #1 ]\!]} 

166: 

167: %%Typefaces%%

168: \def\ttt{\texttt} 

169: \def\mtt{\mathtt} 

170: \def\tsc{\textsc}

171: \def\tsf{\textsf} 

172: \def\mrm{\mathrm}

173: \def\msf{\mathsf} 

174: \def\mbf{\mathbf} 

175: \def\tbf{\textbf} 

176: \def\mcl{\mathcal} 

177: \def\mbb{\mathbb} 

178: \def\mfrk{\mathfrak} 

179: \def\scs{\scriptstyle}

180: \def\dps{\displaystyle}

181: 

182: 

183: %%Greek letters%%

184: \def\al{\alpha}

185: \def\ba{\beta}

186: \def\ga{\gamma}

187: \def\Ga{\Gamma}

188: \let\da\delta

189: \def\eps{\epsilon}

190: \def\ka{\kappa}

191: \def\la{\lambda} 

192: \def\La{\Lambda} 

193: \def\sig{\mat{\sigma}}

194: \def\ta{\theta}

195: 

196: 

197: %%Bold letters%%

198: 

199: \newcommand{\bfa}{\ensuremath{\mathbf{a}}\xspace}

200: \newcommand{\bfb}{\ensuremath{\mathbf{b}}\xspace}

201: \newcommand{\bfc}{\ensuremath{\mathbf{c}}\xspace}

202: \newcommand{\bi}{\ensuremath{\mathbf{i}}\xspace}

203: \newcommand{\bl}{\ensuremath{\mathbf{l}}\xspace}

204: \newcommand{\bo}{\ensuremath{\mathbf{o}}\xspace}

205: 

206: \newcommand{\bA}{\ensuremath{\mathbf{A}}\xspace}

207: \newcommand{\bB}{\ensuremath{\mathbf{B}}\xspace}

208: \newcommand{\bC}{\ensuremath{\mathbf{C}}\xspace}

209: \newcommand{\bD}{\mathbf{D}}

210: \newcommand{\bE}{\ensuremath{\mathbf{E}}\xspace}

211: \newcommand{\bF}{\mathbf{F}}

212: \newcommand{\bG}{\mathbf{G}}

213: \newcommand{\bH}{\mathbf{H}}

214: \newcommand{\bI}{\mathbf{I}}

215: \newcommand{\bJ}{\mathbf{J}}

216: \newcommand{\bK}{\mathbf{K}}

217: \newcommand{\bL}{\mathbf{L}}

218: \newcommand{\bM}{\mathbf{M}}

219: \newcommand{\bN}{\mathbf{N}}

220: \newcommand{\bO}{\mathbf{O}}

221: \newcommand{\bP}{\mathbf{P}}

222: \newcommand{\bQ}{\mathbf{Q}}

223: \newcommand{\bR}{\mathbf{R}}

224: \newcommand{\bS}{\mathbf{S}}

225: \newcommand{\bT}{\mathbf{T}}

226: \newcommand{\bU}{\mathbf{U}}

227: \newcommand{\bV}{\mathbf{V}}

228: \newcommand{\bW}{\mathbf{W}}

229: \newcommand{\bX}{\mathbf{X}}

230: \newcommand{\bY}{\mathbf{Y}}

231: \newcommand{\bZ}{\mathbf{Z}}

232: 

233: %%Caligraphic letters%%

234: \newcommand{\cA}{\mathcal{A}}

235: \newcommand{\cB}{\mathcal{B}}

236: \newcommand{\cC}{\ensuremath{\mathcal{C}}}

237: \newcommand{\cD}{\mathcal{D}}

238: \newcommand{\cE}{\ensuremath{\mathcal{E}}}

239: \newcommand{\cF}{\mathcal{F}}

240: \newcommand{\cG}{\mathcal{G}}

241: \newcommand{\cH}{\mathcal{H}}

242: \newcommand{\cI}{\mathcal{I}}

243: \newcommand{\cJ}{\mathcal{J}}

244: \newcommand{\cK}{\mathcal{K}}

245: \newcommand{\cL}{\mathcal{L}}

246: \newcommand{\cM}{\mathcal{M}}

247: \newcommand{\cN}{\ensuremath{\mathcal{N}}}

248: \newcommand{\cO}{\mathcal{O}}

249: \newcommand{\cP}{\ensuremath{\mathcal{P}}}

250: \newcommand{\cQ}{\mathcal{Q}}

251: \newcommand{\cR}{\mathcal{R}}

252: \newcommand{\cS}{\ensuremath{\mathcal{S}}}

253: \newcommand{\cT}{\mathcal{T}}

254: \newcommand{\cU}{\mathcal{U}}

255: \newcommand{\cV}{\mathcal{V}}

256: \newcommand{\cW}{\mathcal{W}}

257: \newcommand{\cX}{\mathcal{X}}

258: \newcommand{\cY}{\mathcal{Y}}

259: \newcommand{\cZ}{\mathcal{Z}}

260: 

261: 

262: \def\lastname{D'Hondt and Sadrzadeh}

263: \begin{document}

264: 

265: 

266: 

267: 

268: \begin{frontmatter}

269: 

270: 

271:   \title{Classical knowledge for quantum security ({\tt \large extended abstract})} 

272:      

273: \author{Ellie D'Hondt\thanksref{myemail}}

274: \address{Vrije Universiteit Brussel \& FWO, Belgium}

275: 

276: \author{Mehrnoosh Sadrzadeh \thanksref{vemail}}

277: \address{ Laboratoire Preuves Programmes et Syst\`{e}mes, Universit\'{e} Paris 7, France}

278:  

279:   

280:  

281: \thanks[vemail]{Email:

282:     \href{mailto:mehrs@comlab.ox.ac.uk} {\texttt{\normalshape

283:         mehrs@comlab.ox.ac.uk}}}

284:  \thanks[myemail]{Email:

285:     \href{mailto:Ellie.DHondt@vub.ac.be} {\texttt{\normalshape

286:         Ellie.DHondt@vub.ac.be}}}

287: 

288:         

289: \begin{abstract} 

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

291: \end{abstract}

292: 

293: \begin{keyword}

294: Quantum cryptography, distributed measurement calculus, algebraic information update.

295: \end{keyword}

296: 

297: \end{frontmatter}

298: 

299: 

300: 

301: \section{Introduction}

302: Quantum communication is an inseparable  part  of  quantum computing: it offers solutions to the risks caused by the exponential speed-up in the power of  adversaries,  which is in turn caused  by quantum algorithms. While some advances have been made in the area of formal verification of quantum communication protocols~\cite{Gay05}, no applicable formal framework has yet been suggested for  their automatic cryptanalysis.  This is contrary to the fact that,  similar to the situation in classical security,  attacks have been  discovered on proven-to-be-safe quantum protocols.

303: 

304: 

305: In this paper, we present a  decision procedure  to verify wether a protocol satisfies an epistemic security property. Our procedure  derives  knowledge properties of agents   from  the set of  dynamic and epistemic traces of the protocol.  The \emph{dynamic traces}  are generated  from the protocol specification  by operational rules of   distributed measurement calculus (DMC)~\cite{Danos05b}.  These   are then expanded to the \emph{epistemic traces} using  \emph{appearances} of agents about the actions of the protocol. The appearances are derived from the  safety assumptions of the communication channels according to a set  of  rules.  Our  notions of knowledge and time are classical and have been used in  the formal analysis of classical  protocols, for example in the Halpern style models of~\cite{Prakash,Danos07} and in the algebraic Epistemic Systems of~\cite{BCS2,SadrThesis}. 

306: 

307: Both the DMC model and the algebra have been  previously used to  analyze the security of quantum key distribution (QKD) and its attacks~\cite{Danos07,DHondt05c,SadrAAAI}. 

308: The setting of this paper has advantages over both these attempts. First, we rely on the already existing rules of the semantics of DMC, as opposed to adding axioms for quantum mechanics to the algebra as pursued in~\cite{SadrAAAI}. Second, we use the algebraic axiomatics of dynamic and epistemic adjunctions  to derive knowledge properties of the protocol, as opposed to model-checking them by traversing the tree of the protocol as done in~\cite{Danos07,DHondt05c}. Third,  we set the actions of  the adversary in a compositional way using the appearance maps of the algebra, as opposed to ad-hocly adding them to the specification of the protocol as suggested in~\cite{Danos07,DHondt05c}. 

309: 

310: We prove that our decision procedure is sound and terminating with regard to the pair of a DMC model and the algebraic axiomatics of Epistemic Systems. We apply our decision procedure to   a new quantum secret sharing (QSS) protocol, which is  based on graph states and has been proposed recently in~\cite{Markham08}. For this protocol, we develop epistemic properties and prove them  for three kinds of  assumptions on the quantum channels: safe, unsafe with non-suspicious agents, and unsafe with suspicious agents. We show that in the second case, the protocol does not satisfy its desired epistemic property and is thus not secure, moreover, we discover the path of an intercept-exchange attack that caused this insecurity.  A full analysis of the safety assumptions  of all the channels and their impact on the security properties needs automation, which constitutes on going work. Also, we have only been working on a one-round basis and indeed, for a full analysis of protocols one needs to run the protocol in many runs and then use probabilities, for instance on the knowledge modalities. This would be a natural and exciting extension of the currently proposed framework. 

311: 

312: 

313: 

314: In a nut shell, our framework  is obtained by merging the model checking approach of~\cite{DHondt05c,Danos07} and the algebraic axiomatics of~\cite{SadrAAAI}.   The former is based on a distributed extension~\cite{Danos05b} for an assembly language~\cite{Danos04b} that universally models computations of the one way model.  Its  knowledge operator is defined over Kripke  structures in the style of  Fagin et al~\cite{FH} by using equivalence relations on the states. Reasoning about properties of a protocol is done on the state space of this structure using a  logic with temporal and epistemic operators. 

315: %These Kripke structures are built per protocol from  the special-purpose language of distributed quantum computations and by following the small-step semantics defined for this language.  The configuration space contains information about the communications,  computations  and local and global resources of a protocol. 

316: The latter  is based on   the Stone-like duals  of these relational systems and moreover, following~\cite{CoeckeMS},  a quantale structure is assumed  on the actions. This setting consists of a pair of a quantale of classical and quantum actions and its right module of bits and qubits involved in a protocol. The pair is endowed with a family of join-preserving maps, one for each agent involved in the protocol.  The right adjoints  to these endomorphisms give rise to a very useful  notion of knowledge, both on propositions of module and actions of quantale. 

317: %The reasoning power of the algebra comes from these adjunctions, together with the right adjoint to the action of the quantale on the module and the weak distributivity of these endomorphisms over the action and the multiplication of the quantale. 

318: 

319: 

320: \section{Decision Procedure}

321: The procedure has three main steps. 

322: First, we write as program in the language of  the distributed measurement calculus (DMC) to implement the specification of the  quantum protocol  and generate a set of  \emph{dynamic traces} for it. This is done   by executing the rules of the operational semantics. of DMC   Second, we write  formulae with dynamic and epistemic modalities  to expresses security properties of the protocol. This is done  in the algebraic  syntax  of Epistemic Systems. Finally,  we apply an algebraic rewrite system to decide wether the protocol satisfies the properties. 

323: 

324: \smallskip

325: \noindent

326: {\bf Step (1)  Specify and produce dynamic traces in DMC.}\\

327: Programs of  DMC are implemented as \emph{networks of agents}. A {network of agents}  is denoted by $\cN$ and  is defined as follows 

328: \begin{center}\begin{minipage}{13cm}

329: \[

330: \cN= \gket \given \bA(Q).\cE\nr \bB(Q').\cE'\dots\quad\text{.}

331: \]\end{minipage}\end{center}

332: 

333: \medskip

334: \noindent

335: It consists of  a  set of agents acting in parallel (denoted by $|$)  on a given entanglement resource \gket.

336: An \emph{agent} $\bA(Q).\cE$ is specified by a name $\bA$, a set $Q$ of qubits it owns, and an event sequence $\cE$. The event sequence  can be a computation in the measurement calculus, a classical message reception $\cci x$ and sending $\cco y$, or  a qubit reception $\qci q$ and sending $\qco q'$. Note that, contrary to the original definitions in~\cite{Danos05b} we now write specifications from left to right; also agents may have extra classical parameters $a$, written as $A(a,Q)$.

337: As an example, here is one round of Ekert's implementation of QKD:

338: \begin{center}\begin{minipage}{13cm}

339: \[

340: QKD=\et 12 \| \bA(a,1).[H_{1}^{a};M_{1};\cco a; \cci b] \nr \bB(b,2).[H_{2}^{b};M_{2}; \cci a;\cco b] 

341:  \text{  .}

342: \]\end{minipage}\end{center}

343: 

344: \medskip

345: The set of traces of a program are generated by following the rules of the small-step semantics as specified in \cite{Danos05b}, but moreover, we work with projections, annotate actions with agents that performed them, and name the preparation actions of the initial entanglement resource \gket \ and  the distribution actions of qubits.  For example,  $P_i^{A,\alpha}$ stands for the spin $\alpha$ projection of qubit $i$ done by agent $A$ and $N_i^C$ is the preparation of qubit $i$ by agent $C$. The preparation actions are made explicit by juxtaposing them  to the left most of the traces; for QKD the

346: entanglement resource $\et 12$ is created by applying $N^C_1; N^C_2; E^C_{1 2}$ to a 2-qubit system $q_{1}\ox q_{2}$, where $N$ is preparation in the $\p$ state and $C$ is the agent who prepared the entanglement resource.  Distributing these qubits to agents $A$ and $B$ is denoted by a quantum broadcast action $\qcio^C_X q_i$, which stands for agent $C$ sending  qubit $q_i$ to agent $X$ and agent $X$ receiving it from him. This is a shorthand for a quantum send $\qco^C_X q_i$ and a quantum receive $\qci^X_C q_i$.  Similarly, we also shorthand a classical send $\cco^C_X  a$ and receive $\cci^X_C a$ to a broadcast $\ccio^C_X a$.

347: 

348:  According to these conventions two of the four possible traces for a successful run of QKD  become as follows

349: 

350: 

351: \begin{center}\begin{minipage}{13cm}

352: \[

353: \pi= N^C_1 ; N^C_2 ; E_{1,2}^{C} ;  \qcio^C_A\,  q_1; \qcio^C_B\,  q_2 ; P_1^{A, X} ; P_2^{B,X} ; \ccio^A_B\,  a ;  \ccio^B_A\,  b\quad\text{,}

354: \]

355: 

356: \medskip

357: \[

358: \pi'= N^C_1 ; N^C_2 ; E_{1,2}^{C} ;  \qcio^C_A\,  q_1; \qcio^C_B\,  q_2  ; P_1^{A, Z} ; P_2^{B,Z} ; \ccio^A_B\,  a ;  \ccio^B_A\,  b\quad \text{.}

359: \]\end{minipage}\end{center}

360: 

361: \bigskip

362:  \noindent

363: {\bf Step (2)  Write security properties in Epistemic Systems.}\\

364: The input to the rewrite  system is an expression of the form 

365: \[

366: l \vdash r

367: \]

368:  where $l$ is  the initial state and $r$ is  an epistemic property that  contains the disjunction of  dynamic traces  produced above. An example is the following expression  

369: \[

370: q_i \vdash [\pi]\Box_A \Box_A s_i^j

371: \]

372: which  is  read as

373:  

374: \begin{center}

375:  \fbox{\begin{minipage}{12cm}

376:  \begin{center} After running the trace $\pi$ of  the protocol on qubit $q_i$, agent $A$ knows that $B$ knows that the value of bit $i$ is $j$.\end{center}\end{minipage}}\end{center}

377:  

378:  \noindent

379:   The $l$ and $r$ expressions are   generated as follows:

380: \begin{center}\fbox{\begin{minipage}{13cm}

381:  \begin{itemize}

382:  \item The initial state  $l$ is made of  propositions $m$ that are formed by  closing  atomic classical and quantum variables $s_i^j$ and $q_i$ under $\neg, \wedge, \vee$ and logical constants $\bot, \top$. The variables are generated   as follows

383:  \[

384:  \kappa ::= s_i^j \mid q_l \mid q_l \otimes q_w

385:  \] 

386: 

387: \item The epistemic property $r$ is generated  as follows

388: \[

389: r ::= m \mid [\pi]m \mid \Box_A (m)

390: \]

391: where $\Box_A (m)$ is the epistemic modality and for $\pi$ a dynamic trace  $[\pi]m$ is the dynamic modality.

392: \end{itemize}\end{minipage}}\end{center}

393: One such expression for Ekert's QKD is

394: \begin{center}\begin{minipage}{13cm}

395: \[

396: q_1 \otimes q_2 \vdash \left[

397:  N^C_1 ; N^C_2 ; E_{1,2}^{C} ;  \qcio^C_A\,  q_1; \qcio^C_B\,  q_2 ; P_1^{A, X} ; P_2^{B,X} ; \ccio^A_B\,  a ;  \ccio^B_A\,  b

398:  \right]\Box_A \Box_B (s_1^0 \wedge s_2^0)

399: \]

400: \end{minipage}\end{center}

401: 

402: \medskip

403: \noindent

404:  Proving this property together with a permutation of it  for   $B$, that is

405:  \begin{center}\begin{minipage}{13cm}

406: \[

407: q_1 \otimes q_2 \vdash \left[

408: N^C_1 ; N^C_2 ; E_{1,2}^{C} ;  \qcio^C_A\,  q_1; \qcio^C_B\,  q_2 ; P_1^{A, X} ; P_2^{B,X} ; \ccio^A_B\,  a ;  \ccio^B_A\,  b

409:  \right]\Box_B \Box_A (s_1^0 \wedge s_2^0)

410: \]

411: \end{minipage}\end{center}

412:  will imply  that $A$ and $B$\emph{ share} a piece of data, which is the results of each other's measurements, that is $ (s_1^0 \wedge s_2^0)$. The sharing property is expressed by the nested knowledge property, that $A$ knows that $B$ knows it, and vice versa \footnote{It is arguable  wether one has to nest the knowledge modalities infinitely many times and thus use the common knowledge  operator to express the sharing property, but for now we restrict ourselves to a two level nesting.}. That the data is \emph{secret} is proved by showing that an adversary $E$ does not know it, that is the following expression

413:  \begin{center}\begin{minipage}{13cm}

414: \[

415: q_1 \otimes q_2 \vdash \left[

416: N^C_1 ; N^C_2 ; E_{1,2}^{C} ;  \qcio^C_A\,  q_1; \qcio^C_B\,  q_2 ; P_1^{A, X} ; P_2^{B,X} ; \ccio^A_B\,  a ;  \ccio^B_A\,  b

417:  \right] \neg \Box_E (s_1^0 \wedge s_2^0)

418: \]

419: \end{minipage}\end{center}

420: 

421: \bigskip

422:  \noindent

423: {\bf Step (3). Generate Epistemic traces and verify the property.}\\

424: We proceed by analyzing uncertainty of agents about the states and actions of protocols. These are referred to as  \emph{appearance} maps  and are denoted by $f_A$ for an agent $A$. They encode all possible actions or propositions that appear possible to an agent, given the action that is happeneing or the proposition that is true in reality, we refer the reader to~\cite{BCS2,SadrThesis} for discussions and examples. Here, we treat these maps  more practically and introduce a general set of rules to generate them. These  rules are presented  below.

425: 

426: \begin{center}

427: \begin{enumerate}

428: \item The  agents have no uncertainty about the steps of the protocol they are involved in.

429: 

430: 

431: \item Qubits are encoded as black boxes and thus appear as they are, that is as identity to all agents.  Classical bits appear as either 0 or 1 to agents.

432: 

433: 

434: \item  The owner of an action has no uncertainty about his actions, but is uncertain about other agents' actions. His appearances of these latter actions are generated by instantiating their  variables.  

435: 

436: 

437: \item  There is only one adversary present in each protocol. This adversary can intercept the unsafe channels, either quantum or classical, by stopping the messages, changing the content of the messages, creating new messages and sending them. On a quantum channel, the change of the content of the message is done by   measuring the sent qubit and  the creation of new messages by preparing fresh qubits. On the classical channel, the change is simply affected by reading and writing the values of the bits. 

438: 

439: 

440: \item On the safe channels, the adversary can either be passive or not present at all.  In the latter case, he cannot even see if messages are passing through and what is their content.  In the former case, on a classical channel, he can see the value of the bits  as well as the sender and receiver of each message, but cannot change anything. On a quantum channel, he can only see that a qubit is passing, but cannot see its state. 

441: 

442: 

443: \item Communication actions on a safe channel are either public or private announcements to a subgroup of agents. The former appears as identity to all agents, whereas the latter is  identity only to the insiders in the group, and either as nothing or all possible choices to the outsider agents. On an unsafe channel, the announcement actions are treated as   separate send and receive actions.

444: 

445: 

446: \item Honest agents may suspect the interception actions of the adversary. If they do so, these actions  appear to them as either happened or not. If they do not, they appear to them as the neutral action in which nothing happens.

447: \end{enumerate}\end{center}

448: 

449: \medskip

450: \noindent

451: For example, the appearances of the projection action $P_1^{A, X}$ in our above example traces are  as follows

452: 

453: \begin{minipage}{13cm}

454: \[

455: f_A(P_1^{A, X}) = P_1^{A, X}, \qquad f_B(P_1^{A, X}) = P_1^{A, X} \vee P_1^{A, -X} \vee P_1^{A, Z} \vee P_1^{A, -Z}\quad .

456: \]

457: \end{minipage}

458: 

459: \medskip

460: \noindent

461: The appearances of the communication actions depend on the safety assumptions of the channel in which they take place. For example, if the channel is safe, they are treated as broadcasts otherwise as separate send and receive actions.  We present  a detailed example on those in the last section. 

462: 

463: \medskip

464: \noindent

465: Due to space limits we cannot present the rewrite rules;  they are similar to the system  presented in~\cite{SimonSadr}. By applying them, one first  eliminates the    logical connectives  $\wedge, \vee,\Box_A, [\  ]$ and  then the classical  and quantum communication actions. The output is a  set of \emph{atomic expressions}, defined as follows

466: \begin{definition}

467: An expression  $l  \vdash r$ is atomic iff $l$ is a   quantum state followed by a sequence of atomic quantum actions and $r$ is an atomic classical or quantum state. 

468: \end{definition}

469: 

470: \noindent

471: For instance, for a safe quantum channel, the atomic form of the our sharing property is 

472: \[

473: (q_1 \otimes q_2)  (N^C_1 ; N^C_2 ; E_{1,2}^{C} ; P_1^{A, X} ; P_2^{B,X}) \vdash s_1^0 \wedge s_2^0

474: \]

475: These  atomic expressions may contain new epistemic uncertainties and thus will need to be  verified against  our  operational semantics.  For this purpose, we introduce below  the notion of a \emph{well-defined} expression.

476: \begin{definition}

477: An atomic expression $l \vdash r $ is \emph{well-defined} iff $l$ is derivable within the operational semantics of DMC. It is true iff $r$ holds in all configurations resulting from $l$. An epistemic property holds for a protocol whenever  all its well-defined atomic expressions are true. 

478: \end{definition}

479: 

480: \begin{proposition}

481: For a protocol specification $\cN$ and an expression $l \vdash r$ which is built  from the dynamic traces of $\cN$, the process of deciding if the epistemic property in $r$ holds for $\cN$ is terminating  and  sound  with regard to the pair of an Epistemic System  and a DMC model.  

482: \end{proposition}

483: \noindent

484: {\bf  Proof.} These  follow from image finiteness of appearances of actions and propositions, together with  soundness and termination of the rewrite system of Epistemic Systems and the DMC model~\cite{Danos05b,SimonSadr}.  

485: 

486: %Completeness would be more challenging but at the same time more interesting, for example, part of  it can be proven  by constructing an algebra of classical and quantum data and actions from the patterns of DMC.   For the other part, one needs to show that the language of security properties mentioned above indeed forms an epistemic system. That it forms a subset of terms of an epistemic system is obvious, but the full equivalence needs addition of more rules (for the terms not considered in the current set of rules) in the decision procedure. Alternatively, one may keep  the existing set of rules as they are, but investigate what kind of sub-algebra they form.

487:  

488:  \section{Case study: quantum secret sharing}

489: 

490: We apply our procedure  to the quantum secret sharing (QSS) protocol recently established in \cite{Markham08}. In secret sharing a dealer holds a secret bit which he wants to send to $n$ players, such that at least $k$ players are needed to reconstruct the secret. The problem is well-known in the  classical settings and solvable for all $(n,k)$. In the quantum case, only the  $(n, n)$ case has been solved for the  GHZ-type entanglement \cite{Xiao04}. The work in \cite{Markham08} uses instead graph states and thus is more suitable for modelling  in our measurement-based setting. Moreover, it generalizes  the quantum key distribution protocols and simplifies their proofs. We analyze and prove some of the epistemic properties of the QKS component of the $(3,5)$ case, where a particular graph state is used to establish a secret key between three players and the dealer in one go (as opposed to via several 2-party QKD protocols). This key will then be used to distribute a secret using the other components of the protocol. 

491: 

492: \begin{center}

493: \scalebox{.60}{\includegraphics{G35.pdf}}

494: %\label{finallevel}

495: \end{center}

496: The recource required for the protocol is the graph state shown above, henceforward called $G(3,5)$. It is prepared following the usual procedure for graph states, that is

497: \begin{center}

498: \begin{minipage}{13cm}

499:  \[

500: G(3,5)= (N_{1};\dots ;N_{5};N_{6};\prod_{e_{ij}}E_{ij})  \otimes_{i= 1}^6 q_i \\; \text{,}

501:  \]

502:  \end{minipage}\end{center}

503:  

504: 

505:  \noindent

506: where  $e_{ij}$ is the set of edges. The protocol proceeds as follows:

507: 

508: 

509: 

510: \hspace{-0.8cm}\fbox{\begin{minipage}{14cm}

511: \begin{description}

512: \item[Step 1.] The dealer prepares $G(3,5)$, sends each agent a qubit $q_{i}$ together with an agent identity $i$.

513: 

514: 

515: \item [Step 2.] The dealer measures his qubit in the $Y$ or $Z$ basis randomly and broadcasts his measurement basis.

516: 

517: 

518: \item [Step 3.] Each participating player measures his qubit  in the $X$,  $Y$ or $Z$ basis randomly, then broadcasts his identity and measurement basis.

519: 

520: 

521: \item [Step 4.] Depending on these messages, each agent determines if the run was successful as follows: 

522: \begin{itemize}

523: \item If the participating agents are neighbours, then we have $ijk=i(i+1)(i+2)$; this is the case for  the following  measurement combinations 

524: \[

525: M_{6}^{Z}M_{i}^{Z}M_{j}^{X}M_{k}^{Z} \quad \text{and} \quad M_{6}^{Y}M_{i}^{X}M_{j}^{Y}M_{k}^{X} \; \text{.}

526: \]

527: \item If they are in a so-called T-shape,  we have $ijk=i(i+1)(i+3)$; this is the case for the following measurement combinations 

528: \[

529: M_{6}^{Z}M_{i}^{X}M_{j}^{Y}M_{k}^{Y}  \quad \text{and} \quad M_{6}^{Y}M_{i}^{Y}M_{j}^{Z}M_{k}^{Z} \; \text{.}

530: \]

531: \end{itemize}

532: \item [Step 5.] For a successful run, measurement outcomes are correlated as $

533: s_{6}=s_{i}\oplus s_{j}\oplus s_{k}$.

534: Players use their secure classical channels to exchange measurement outcomes and determine if $s=s_{6}$, hence establishing a shared key with the dealer. 

535: \end{description}\end{minipage}}

536: 

537: \smallskip

538: We refrain from giving the full specification of the QSS network and move straight on to its traces, where we  treat all the communication actions as broadcasts and later on  break them to separate send and receive actions, as necessary and according to the safety assumptions of their channels.   Whenever the subscript of a broadcast action is missing, e.g. in $\ccio^D a$ it means that the broadcast is a public action that can be listened to by everyone.  A typical trace for a successful run of QSS is as follows

539: 

540: \begin{center}

541: \begin{minipage}{13cm}

542: $$

543: \begin{array}{rll}

544: \pi = & N^D_{1};\dots ;N^D_{6};\prod_{e_{ij}}E^D_{ij}&\text{(preparation)} \\

545: &(\qcio^D_1  q_{1})\dots(\qcio^D_5 q_{5}) &\text{(private broadcast of qubits)}\\

546: & P_6^{D, \pm a}P_i^{ A_i, \pm b}P_j^{ A_j, \pm c}P_k^{A_k,\pm f}&\text{(measurement projections)}\\

547: & \ccio^D a ; \ccio^{A_i} b ; \ccio^{A_j} c ; \ccio^{A_k} c &\text{(public broadcast of measurement bases)}\\

548: & (\ccio^{A_i}_{A_j,A_k} s_{i})(\ccio^{A_j}_{A_i,A_k} s_{j})(\ccio^{A_k}_{A_i,A_j} s_{k})&\text{(private broadcast of player's mes. outcomes)}.

549: \end{array}

550: $$

551: \end{minipage}\end{center}

552: 

553: \medskip

554: \noindent

555: Here $a \in \ens{X,Y}, b,c,f \in \ens{X,Y,Z}$ are measurement basis, $\qcio^{D}_{i} $ is the quantum message passing from $D$ to $A_i \in \{A_1, \cdots, A_5\}$ denoting the 5 players, and $\ccio^{A_i}_{\beta}$ is the private announcement from player $A_i$ to the group $\beta \subseteq \{A_1, \cdots, A_5\}$. We omit  the calculation of the secret key, which is determined  by the following exclusive-or  formula 

556: \[

557: s=s_{i}\oplus s_{j}\oplus s_{k}

558: \]

559:  Successful traces only depend on the chosen values for $a,b,c$ and $f$; one example of such a trace for adjoining agents $A_1$, $A_2$ and $A_3$, owning qubits 1,2 and 3 respectively, is  as follows

560: 

561: \begin{minipage}{13cm}

562: \begin{align*}

563: \pi = \dots&\\

564: & P_6^{D,+Z}P_1^{A_1,-Z}P_2^{A_2,-X}P_3^{A_3,+Z};\\

565: & Z!^{D} ; Z!^{A_1} ; X!^{A_2} ; Z!^{A_3};\\

566: &(\ccio^{A_1}_{A_2,A_3} \; 1)(\ccio^{A_2}_{A_1,A_3} \; 1)(\ccio^{A_3} _{A_1.A_2} \; 0)&

567: \end{align*}

568: \end{minipage}

569: 

570: \subsection{Epistemic Properties}

571: We consider three cases: agents' heaven,   adversary's heaven, and adversary's hell. In the first case the quantum channel is safe, in the second case it is not and the honest agents do not suspect it, in the third case it is not and the honest agents do suspect it. The other channels are assumed to be safe in all three cases.  For each case, we show  how the appearances of agents of actions in the dynamic traces are set. This  is  done according to the safety assumptions on the channel and our rules.  Then we present some of the related epistemic security properties  of each case. 

572: \begin{enumerate}

573: \item {\bf Agents' heaven}\\

574: The appearance of the projections are set according to the rule $(iii)$ of appearances.  Since the channels are safe,  the communication actions on the quantum channel are  treated as public broadcasts and  by rule $(vi)$ and for $\sigma$ an agent they are set as follows

575: \[

576: f_{\sigma}(\qcio^{D} q_i) =   \qcio^{D} q_i

577: \]

578: That is, all the agents are fully aware of the broadcast action and thus have only one possibility in their appearance, the broadcast action itself. 

579:  The communication actions on the classical channels are  private announcements and by rule $(vi)$ their appearances are set as follows,  for  $\beta$ a  subset of players 

580: \begin{center}

581: \begin{minipage}{13cm}

582: \[

583: f_{\sigma} (\ccio _{\beta}^{A_i} s_i^j) = 

584: \begin{cases}

585: \ccio _{\beta}^{A_i} s_i^j & \sigma \in \beta\\

586: &\\

587: \ccio_{\beta}^{A_i} s_i^j \vee \ccio _{\beta}^{A_i} \overline{s}_i^j & \sigma \notin \beta

588: \end{cases}

589: \]\end{minipage}\end{center}

590: This says that the insider agents $\sigma \in \beta$ who receive the sent  bit $s_i^j$, which is either equal to 1 or 0, are fully aware what has happened and thus have only one possibility about the private broadcast action,  that is  the broadcast action itself and thus their appearance is identity. But by rule $(i)$ of appearances, the outsider agents $\sigma \notin \beta$ are only aware that a bit has been privately broadcasted to the subgroup $\beta$ and are uncertain about the value of that bit.  So they consider it possible  that either a bit with value 1 or a bit with value 0 has been privately broadcasted to insider agents in $\beta$. Thus  their appearance is the choice of these two possibilities. 

591:  

592: 

593: Some of the  epistemic properties of interest for our trace $\pi$,  allied players $A_i \in \{A_1,A_2, A_3\}$,  joined with dealer $ \sigma \in \{D, A_1,A_2, A_3\}$   are as follows

594: 

595: \medskip

596: \hspace{-0.3cm}\fbox{

597: \begin{minipage}{12.2cm}

598: \begin{itemize}

599: \item The dealer knows his bit and  binary sum of allied players' bits, i.e.

600: \[

601: \Box_D\,  (s_6^0 \wedge (s_1^{b_1}\oplus  s_2^{b_2} \oplus s_3^{b_3}))\,.

602: \]

603: 

604: 

605: \item Allied players moreover know the value of each single measurement,  i.e.

606: \[

607: \Box_{A_i}\, ( s_6^0 \wedge s_1^{1} \wedge s_2^{1} \wedge s_3^{0})\,.

608: \]

609: 

610: 

611: \item The dealer knows  that the players know his bit and the players know that the dealer knows the sum of their bits,  i.e.

612: \[

613: \Box_D \Box_{A_i}\,  s_6^0 \quad \text{and}\quad \Box_{A_i} \Box_D   (s_1^{b_1}\oplus  s_2^{b_2} \oplus s_3^{b_3})\,.

614: \]

615: 

616: 

617: \item The adversary does not know any of the above,  i.e.

618: \[

619: \neg \Box_E\,  (s_6^0 \wedge (s_1^{b_1}\oplus  s_2^{b_2} \oplus s_3^{b_3}))\,.

620: \]

621: 

622: 

623: \item The dealer and the agents know the above,  i.e.

624: \[

625: \Box_{\sigma} \neg \Box_E\,  (s_6^0 \wedge (s_1^{b_1}\oplus  s_2^{b_2} \oplus s_3^{b_3}))\,.

626: \]

627: \end{itemize}

628: \end{minipage}

629: }

630: 

631: 

632: \vspace{5mm}

633: \item {\bf Adversary's heaven}\\

634: In this case, the quantum channel is not safe and  by rule $(iv)$ the adversary  can intercept the channel.  By rule $(vi)$ since the channel is not safe, we  must break  its broadcasts to  separate send and receive actions. The  appearances of these actions to the agents involved in them (e.g. the appearance of the sent action to the agents  who received it) are not identities any more.   The appearances for  the send of a qubit   are set as follows, where $q_j$ is a new qubit with  $j \geq 7$

635: \begin{center}

636: \begin{minipage}{13cm}

637: \[

638: f_{\sigma'} (\qco ^D_i q_i) =  

639: \begin{cases}

640: \qco ^D_i\,  q_i ; \qci ^E_D\,  q_i ; P_i^{E,e};  N_j^{E,e} ; \qco ^E_i\,  q_j & \sigma' = E\\

641: &\\

642: \qco ^D_i q_i & o.w.

643: \end{cases}

644: \]\end{minipage}\end{center}

645: This says that neither the agents nor the dealer  suspect that $E$ intercepted dealer's sent qubit and thus their appearance of dealer's sent action is (wrongly) identity. Where as in reality, $E$ did the following sequence of interception events, but they only appear to him as identity.

646: \[

647: \qco ^D_i\,  q_i ; \qci ^E_D\,  q_i ; P_i^{E,e};  N_j^{E,e} ; \qco ^E_i q_j  

648: \]

649: According to this sequence of events, $E$ received the dealer's sent qubit $q_i$ that was meant to be received by agent $i$, measured it, then  prepared a corresponding new qubit $q_j$ and sent it to agent $i$.  For the corresponding receive action, it appears to the dealer  that players received the qubit that he sent to them, $f_D (\qci ^{A_i}_D\,  q_i)=\qci ^{A_i}_D\,  q_i$, whereas in reality they receive the qubit sent to them by adversary, $f_{A_i} (\qci ^{A_i}_D\,  q_i)=\qci ^{A_i}_E\,  q_j$.

650: In case the eavesdropper is lucky and chooses the right projection for all three qubits he intercepts, he is able to derive the value of the key. In this case some of the  epistemic properties of interest are

651: 

652: \medskip

653: \hspace{-0.6cm}\fbox{

654: \begin{minipage}{13cm}

655: \begin{itemize}

656: \item   The adversary knows the shared key, i.e. $\Box_E s_6^0 $.

657: 

658: 

659: \item The  players and the dealer wrongly think that he does not know  this, i.e. 

660: \[

661: \Box_{\sigma}  \neg \Box_E s_6^0\,.

662: \]

663: \end{itemize}

664: \end{minipage}}

665: 

666: \medskip

667: \noindent

668: Note that here the adversary has to be more  lucky than in Ekert'91. This is because he has to intercept the qubits of three allied  players instead of one, and has to choose from three measurement bases. 

669: 

670: 

671: \vspace{5mm}

672: \item {\bf Adversary's hell}\\

673: This is the same as above, but the players suspect adversary's actions, that is according to rule $(vii)$,  it appears to them either there was no interception or  there was one and the above sequence of actions took place by the adversary. Thus we obtain

674: 

675: \medskip

676: \begin{minipage}{13cm}

677: \[

678: f_{A_i} (\qco ^D_i\,  q_i) =  \qco ^D_i\,  q_i  \vee (\qco ^D_i\,  q_i ; \qci ^E_D\,  q_i ; P_i^{E,e} ;  N_j^{E,e} ; \qco ^E_i\,  q_j )

679: \]

680: \end{minipage}

681: 

682: \noindent

683: \medskip

684: Similarly, the dealer suspect adversary's actions on the receipt of his sent qubit

685: \begin{center}

686: \begin{minipage}{13cm}

687: \[f_D(\qci ^{A_i}_D\, q_i) = \qci ^{A_i}_D\, q_i \vee (\qci ^E_D\, q_i ; P_i^{E,e};  N_j^{E,e} ; \qco ^E_i q_j ; \qci ^{A_i}_E q_j)

688: \]\end{minipage}\end{center}

689: 

690: \medskip

691: \noindent

692: In this case, an interesting epistemic property would be the following 

693: 

694: \medskip

695: \begin{center}\fbox{

696: \begin{minipage}{12cm}

697: \begin{center} The dealer and the players are  not sure anymore if the adversary knows their secret bit, and thus if the bit can be treated as a secret i.e. \end{center}

698: \[

699: \neg \Box_{\sigma} \neg \Box_E s_6^0\,.

700: \]

701: \end{minipage}}\end{center}

702: \end{enumerate}

703: 

704: 

705: \subsection{Verifying Epistemic Properties}

706: As  examples, we verify two properties: one from the agents' heaven  and one from the adversary's hell. 

707: 

708: \begin{itemize}

709: \item {\bf Agents' heaven} \\From this scenario, we verify the following property

710: \[

711: \otimes_{i= 1}^6 q_i \vdash [\pi] \Box_D \Box_i\,  s_6^0

712: \]

713: The atomic expressions are generated via the following rewritings, where $\alpha_i$'s denote the juxtaposed actions of $\pi$

714: 

715: 

716: \begin{center}

717: \hspace{-1.4cm}{\begin{minipage}{15cm}

718: \begin{align*}

719: \otimes_{i= 1}^6 q_i \vdash [\pi] \Box_D \Box_{A_i}\,  s_6^0& \quad  \leadsto\quad 

720: \otimes_{i= 1}^6 q_i ; \pi \vdash\Box_D \Box_{A_i}\,  s_6^0 \quad \leadsto \quad \\

721: f_{A_i} f_D(\otimes_{i= 1}^6 q_i ; \pi ) \vdash s_6^0  & \quad \leadsto \quad

722:  f_{A_i} f_D(\otimes_{i= 1}^6 q_i) ; f_{A_i} f_{D}(\pi)  \vdash s_6^0 \\

723:  &\quad \leadsto\quad 

724:  f_{A_i} f_{D}(\otimes_{i= 1}^6 q_i) ; f_{A_i} f_{D}(\alpha_1); \cdots ; f_{A_i} f_D(\alpha_n)  \vdash s_6^0.

725: \end{align*}

726: \end{minipage}}\end{center}

727: 

728: 

729: \medskip

730: \noindent

731: By rule $(ii)$ of appearances we have $f_{A_i} f_{D}(\otimes_{i= 1}^6 q_i)  = \otimes_{i= 1}^6 q_i$. By rule $(iv)$ and our assumptions on channels,  we have $f_D(\alpha_i) = \alpha_i$ for $\alpha_{A_i}$ a quantum or broadcast communication action. By rule $(vi)$ for  communication between players we have $f_D(\ccio _{\beta}^{A_i} s_i^j) = \ccio _{\beta}^{A_i} s_i^j \vee \ccio _{\beta}^{A_i} \overline{s}_{i}^j$. Similarly for the projection actions we have 

732: 

733: 

734: \begin{center}

735: \begin{minipage}{13cm}

736: \[f_D(P_6^{D,+Z}) = P_6^{D,+Z}

737: \]

738: and

739: \[

740:  f_D(P_1^{A_1,-Z})  = P_1^{A_1,-Z} \vee P_1^{A_1,+Z} \vee P_1^{A_1,-X} \vee P_1^{A_1,+X} \vee P_1^{A_1,-Y} \vee P_1^{A_1,+Y}\quad \text{.}

741: \]

742: \end{minipage}\end{center}

743: 

744: \medskip

745: \noindent

746: The values for the $f_{A_i}$'s are similarly set.   Substituting these values in the above expression, we first eliminate the traces in which the bases of projections do not match the announced  bases. Next we eliminate the communication actions from these traces whose content do not match the projections. As a result, we obtain a set of atomic expressions, of which only those satisfying $s_{6}^{0}=s_1^{b_1}\oplus  s_2^{b_2} \oplus s_3^{b_3}$ are well-defined in DMC. An example (out of  four) is

747: \begin{center}

748: \begin{minipage}{13cm}

749: \[

750: \otimes_{i= 1}^6 q_i ; N^D_{1};\dots ;N^D_{6};\prod_{e_{ij}}E^D_{ij} ; P_6^{D,+Z}; P_1^{A_1,+Z}; P_2^{A_2,-X}; P_3^{A_3,-Z}  \vdash  s_6^0\quad \text{.}

751: \]

752: \end{minipage}\end{center}

753: This atomic expression is true, since in all its final configurations  $s_6$  is 0, and thus our epistemic property holds for the secret sharing protocol.  

754: 

755: \item

756: {\bf Adversary's hell}\\

757: On the contrary, in the adversary's hell, one    shows that the epistemic property  $\Box_D \neg \Box_E s_6^0$ does not hold and thus $s_6^0$ is not treated a secret anymore. Moreover, we also discover paths of an intercept-change attack for each agent, for example the one for the player $A_1$ contains the following sequence of actions

758: \begin{center}

759: \begin{minipage}{13cm}

760: \[\cdots ; \qco ^D_1\, q_1 ; \qci ^E_1\, q_1; P_1^{E,+Z};  N_7^{E,+Z} ; \qco ^E_1\, q_7; \qci ^{A_1}_E\, q_7; P_7^{A_1,+Z}; \cdots

761: \]\end{minipage}\end{center}

762: In this path, the adversary receives dealer's original qubit $q_1$ that was meant to be received by agent 1, then measures it in basis $Z$ by doing projection $P_1^{E,+Z}$, then prepares a new qubit $q_7$ according to his measurement result and sends it to agent 1. The adversary turns out to be lucky and agent 1 picks the same measurement basis as him, that is $Z$ and does the same projections. The classical result of this projection   will for sure be the same as adversary's but might not the same as the dealer's.   

763: \end{itemize}

764: 

765:  

766:  \section{Conclusion}

767: In this article we proposed a new framework for formal analysis of security issues in quantum cryptographic protocols. Our  framework combines an algebraic rewrite system with a specification language for quantum distributed computations. The former provides machinery to work with uncertainties of agents in a protocol in a compositional way, while the latter inherently encodes the rules of quantum mechanics. Our framework was put to test in the analysis of a recent quantum secret sharing protocol based on graph states, where we proved some epistemic properties of the protocol in the presence and absence of an active adversary and discovered paths of an intercept-exchange attack. 

768:  For a full analysis one needs to generate many more epistemic traces and the need for automation and software implementation  is gravely felt.   A software implementation of the algebra~\cite{SimonSadr} is already in place to handle part of the verification. The construction of a tool that automatically derives the traces and semantics of a protocol is currently underway. 

769: 

770: 

771: 

772: \section*{Acknowledgments}

773:  We had fruitful discussions with V. Danos, P. Panangaden,  D. Markham.  The second author has given talks  on a version of the algebra with some quantum axioms encoded in it, which was  partly based on joint work with E. Kashefi. 

774:  

775: 

776: 

777: \bibliographystyle{entcs}

778: \bibliography{references}

779: 

780: \begin{thebibliography}{}

781: 

782: \bibitem{BaltagMoss}  A. Baltag and L.S. Moss. 'Logics for epistemic

783: programs'. {\em Synthese} {\bf 139}, 2004.

784: 

785: \bibitem{BCS2} A. Baltag, B. Coecke, and M. Sadrzadeh, 'Epistemic actions as resources',  \emph{Journal of  Logic and Computation}  {\bf 17 (3)}, May 2007,  {\tt arXiv:math/0608166}.

786: 

787: \bibitem{Bennett84} C.H. Bennett and G. Brassard, 'Quantum cryptography: public key distribution and coin tossing', in \emph{Proceedings of IEEE international Conference on Computers, Systems and Signal Processing}, Bangalore, India, page 175. IEEE Press, 1984.

788: 

789: \bibitem{CoeckeMS}  {B. Coecke and D. J. Moore and I. Stubbe}, `Quantaloids describing causation and propagation of physical properties', \emph{Foundations of Physics Letters}, {\bf 14},   {2001}.

790: 

791: \bibitem{Danos05b}

792: V. Danos, E. D'Hondt, E. Kashefi, and P. Panangaden, 'Distributed measurement-based quantum computation', in  \emph{Proceedings of the 3rd Workshop on Quantum Programming Languages (QPL05)}, ed. P. Selinger, 2005.

793: 

794:   

795:  \bibitem{Danos04b}

796: V. Danos, E. Kashefi and P.Panangaden, 'The measurement calculus', \emph{Journal of the ACM}, 54(2), 2007.

797: 

798: 

799: \bibitem{Danos07} V. Danos and E. D'Hondt, 'Quantum knowledge for cryptographic reasoning', in

800: \emph{Proc. 3rd International Workshop on Development of Computational Models (DCM07)}, ENTCS (to appear), 2008.

801: 

802: 

803: \bibitem{DHondt05c} E. D'Hondt  and P. Panangaden, 'Reasoning about quantum knowledge', in \emph{Proceedings of the 25th Conference on Foundations of Software Technology and Theoretical Computer Science}, LNCS vol. 382, page 0544c , 2006.

804: 

805: 

806: \bibitem{Ekert91} A. K. Ekert, 'Quantum cryptography based on BellÕs theorem', \emph{Phys. Rev. Lett.}, 67(6):661Ð663, 1991.

807: 

808: 

809: \bibitem{FH} R. Fagin, J. Y. Halpern, Y. Moses and M. Y. Vardi. {\em Reasoning about Knowledge}. MIT Press, 1995.

810: 

811: 

812: \bibitem{Gay05}Simon J. Gay, Rajagopal Nagarajan and Nikolaos Papanikolaou, 'Probabilistic model-checking of quantum protocols', quant-ph/0504007, 2005.

813: 

814:  

815: \bibitem{Markham08} D. Markham, A. Roy and B. Sanders, 'Graph States for Quantum Secret Sharing',  private communication, 2008.

816: 

817:  

818: \bibitem{Nielsen00}

819: M.A. Nielsen and I. Chuang,\emph{Quantum computation and quantum information}, Cambridge university press, 2000.

820: 

821:  

822: \bibitem{Prakash}   P. Panangaden and K. Taylor, 'Concurrent Common Knowledge: Defining Agreement for Asynchronous Systems', \emph{Journal of Distributed Computing} {\bf  6}, 1992.

823: 

824: 

825: \bibitem{SimonSadr} S. Richards and  M. Sadrzadeh, `{\tt Aximo}: Automated Axiomatic Reasoning for Information Update', \emph{Proceedings of the 5th workshop on Methods for Modal Logic}, \'{E}cole normal sup\'{e}rieure de Cachan, Nov 2007, to appear in \emph{Electronic Notes in Theoretical Computer Science}.

826: 

827: 

828: \bibitem{SadrAAAI} M. Sadrzadeh, `High-Level Quantum Structures in Linguistics and Multi-Agent Systems',  AAAI Press, Proceedings of AAAI Spring Symposium on {Q}uantum {I}nteraction, 2007.

829: 

830: 

831: \bibitem{SadrThesis} M. Sadrzadeh, 'Actions and Resources in Epistemic Logic', Ph.D. Thesis, University of Quebec at Montreal, 2005, {\tt \small http://eprints.ecs.soton.ac.uk/12823/01/all.pdf}.

832:   

833: 

834: \bibitem{Xiao04} L. Xiao, G. Gong, F-G. Deng, and J-W. Pan. 'Efficient multiparty quantum-secret-sharing schemes', Phys. Rev. A, 69.

835: 

836: \end{thebibliography}

837: 

838: 

839: \end{document}

840: