Techniques for Design and Validation of Quantum Protocols

by Nikolaos Papanikolaou
Abstract:
The objective in this thesis is to perform formal specification and automated validation of the class of protocols associated with quantum cryptography. Current analyses and proofs regarding quantum cryptographic protocols and their security are information-theoretic and also require in-depth understanding of the underlying physics. The alternative approach presented here involves the use of computer modelling languages and verification software. In particular, the logical model checker SPIN and the probabilistic model checker PRISM are used to analyse quantum key distribution, entanglement and quantum teleportation. The value of our approach lies not only in the fact that it is conceptually simpler than existing proofs, but in that it allows us to disambiguate protocol definitions and to assess their properties in various circumstances. By varying the values of certain parameters, different attacks on the protocols can be attempted and implementation specific attributes can be analysed. The quantum key distribution protocol13 BB84 has been proved to be unconditionally secure against all types of eavesdropping. Although a general proof of this result is extremely hard to generate automatically, it is possible to develop specific protocol attacks and validate the protocol by computer. Assuming two types of eavesdropping attack (intercept-resend and random-substitute), we have used the prism tool to compute exactly the probability of successful eavesdropping, and found it to diminish as the number of transmitted qubits is increased. This result is linked to Mayers’ security criteria for BB84. Also, we briefly describe a new quantum protocol definition language, named qSpec. The recent CQP process algebra, due to Nagarajan and Gay, is reviewed and examples of its application are provided. Alternative formalisms and validation tools are discussed, including QPAlg, PROBMELA and probUSM, the logic of knowledge and time for quantum systems due to Van der Meyden, and the QCSim simulator.
Reference:
Techniques for Design and Validation of Quantum Protocols (Nikolaos Papanikolaou), Master’s thesis, Department of Computer Science, University of Warwick, 2004.
Bibtex Entry:
@MASTERSTHESIS{Papanikolaou2004a,
  author = {Nikolaos Papanikolaou},
  title = {Techniques for Design and Validation of Quantum Protocols},
  school = {Department of Computer Science, University of Warwick},
  year = {2004},
  abstract = {The objective in this thesis is to perform formal specification and
	automated validation of the class of protocols associated with quantum
	cryptography. 
	
	
	Current analyses and proofs regarding quantum cryptographic protocols
	and their security are information-theoretic and also require in-depth
	understanding of the underlying physics. The alternative approach
	presented here involves the use of computer modelling languages and
	verification software. In particular, the logical model checker SPIN
	and the probabilistic model checker PRISM are used to analyse quantum
	key distribution, entanglement and quantum teleportation. 
	
	
	The value of our approach lies not only in the fact that it is conceptually
	simpler than existing proofs, but in that it allows us to disambiguate
	protocol definitions and to assess their properties in various circumstances.
	By varying the values of certain parameters, different attacks on
	the protocols can be attempted and implementation specific attributes
	can be analysed. 
	
	
	The quantum key distribution protocol13 BB84 has been proved to be
	unconditionally secure against all types of eavesdropping. Although
	a general proof of this result is extremely hard to generate automatically,
	it is possible to develop specific protocol attacks and validate
	the protocol by computer. Assuming two types of eavesdropping attack
	(intercept-resend and random-substitute), we have used the prism
	tool to compute exactly the probability of successful eavesdropping,
	and found it to diminish as the number of transmitted qubits is increased.
	This result is linked to Mayers' security criteria for BB84. Also,
	we briefly describe a new quantum protocol definition language, named
	qSpec. The recent CQP process algebra, due to Nagarajan and Gay,
	is reviewed and examples of its application are provided. Alternative
	formalisms and validation tools are discussed, including QPAlg, PROBMELA
	and probUSM, the logic of knowledge and time for quantum systems
	due to Van der Meyden, and the QCSim simulator.},
  owner = {Nick},
  timestamp = {2010.06.20},
  url = {../files/nmsc.pdf}
}