The Library
Techniques for design and validation of quantum protocols
Tools
Papanikolaou, Nikolaos K. (2004) Techniques for design and validation of quantum protocols. MSc thesis, University of Warwick.
|
PDF
WRAP_cs-rr-413.pdf - Requires a PDF viewer. Download (697Kb) | Preview |
Official URL: http://webcat.warwick.ac.uk/record=b1782925~S1
Abstract
Our 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 protocol 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.
Item Type: | Thesis (MSc) | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software Q Science > QC Physics |
||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
Library of Congress Subject Headings (LCSH): | Information theory -- Research, Cryptography, Quantum computers, Data encryption (Computer science), Quantum communication | ||||
Series Name: | Department of Computer Science Research report | ||||
Publisher: | University of Warwick. Department of Computer Science | ||||
Official Date: | September 2004 | ||||
Dates: |
|
||||
Number: | Number 413 | ||||
Number of Pages: | 125 | ||||
DOI: | CS-RR-413 | ||||
Institution: | University of Warwick | ||||
Theses Department: | Department of Computer Science | ||||
Thesis Type: | MSc | ||||
Status: | Not Peer Reviewed | ||||
Publication Status: | Unpublished | ||||
Supervisor(s)/Advisor: | Nagarajan, Rajagopal | ||||
Extent: | xv, 107 p. | ||||
Language: | eng | ||||
Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year