2009 |
|
| 17. | Mont, Marco Casassa; Pearson, Siani; Creese, Sadie; Goldsmith, Michael; Papanikolaou, Nick Towards an Integrated Approach to the Management, Specification and Enforcement of Privacy Policies Inproceedings Proceedings of W3C Workshop on Access Control Application Scenarios, Abbaye de Neumünster, Luxembourg, 2009. Abstract | Links | BibTeX | Tags: @inproceedings{CasassaMont2009, title = {Towards an Integrated Approach to the Management, Specification and Enforcement of Privacy Policies}, author = {Marco Casassa Mont and Siani Pearson and Sadie Creese and Michael Goldsmith and Nick Papanikolaou}, url = {../files/W3c-final.pdf}, year = {2009}, date = {2009-01-01}, booktitle = {Proceedings of W3C Workshop on Access Control Application Scenarios}, address = {Abbaye de Neumünster, Luxembourg}, abstract = {We make the case for an integrated approach to privacy management within organisations. Current approaches to privacy management are either too high-level, enforcing privacy of personal data using legal compliance, risk and impact assessments, or too low-level, focusing only on the technical implementation of access controls to personal data held by an enterprise. High-level approaches tend to address privacy as an afterthought in ordinary business practice, and involve ad hoc enforcement practices; low-level approaches often leave out important legal and business considerations. As part of the EnCoRe project we are developing a methodology which tries to bridge the gap between privacy risk and impact assessment with the technical management of privacy policies. We offer our thoughts on how a conceptual model might be devised as a means of expressing policy requirements as well as users' privacy preferences and offer a way to bridge the gap described above.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We make the case for an integrated approach to privacy management within organisations. Current approaches to privacy management are either too high-level, enforcing privacy of personal data using legal compliance, risk and impact assessments, or too low-level, focusing only on the technical implementation of access controls to personal data held by an enterprise. High-level approaches tend to address privacy as an afterthought in ordinary business practice, and involve ad hoc enforcement practices; low-level approaches often leave out important legal and business considerations. As part of the EnCoRe project we are developing a methodology which tries to bridge the gap between privacy risk and impact assessment with the technical management of privacy policies. We offer our thoughts on how a conceptual model might be devised as a means of expressing policy requirements as well as users' privacy preferences and offer a way to bridge the gap described above. |
| 16. | Papanikolaou, Nikolaos Model Checking Quantum Protocols PhD Thesis Department of Computer Science, University of Warwick, 2009. Abstract | Links | BibTeX | Tags: @phdthesis{Papanikolaou2009, title = {Model Checking Quantum Protocols}, author = {Nikolaos Papanikolaou}, url = {../files/nphd.pdf}, year = {2009}, date = {2009-01-01}, school = {Department of Computer Science, University of Warwick}, abstract = {This thesis describes model checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of a practical model checker, QMC, for quantum protocols. In our framework, we assume that the quantum operations performed in a protocol are restricted to those within the stabilizer formalism; while this particular set of operations is not universal for quantum computation, it allows us to develop models of several useful protocols as well as of systems involving both classical and quantum information processing. We detail the syntax, semantics and type system of QMC's modelling language, the logic QCTL which is used for verification, and the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to a number of case studies.}, keywords = {}, pubstate = {published}, tppubtype = {phdthesis} } This thesis describes model checking techniques for protocols arising in quantum information theory and quantum cryptography. We discuss the theory and implementation of a practical model checker, QMC, for quantum protocols. In our framework, we assume that the quantum operations performed in a protocol are restricted to those within the stabilizer formalism; while this particular set of operations is not universal for quantum computation, it allows us to develop models of several useful protocols as well as of systems involving both classical and quantum information processing. We detail the syntax, semantics and type system of QMC's modelling language, the logic QCTL which is used for verification, and the verification algorithms that have been implemented in the tool. We demonstrate our techniques with applications to a number of case studies. |
| 15. | Papanikolaou, Nick Security versus Quantum Computers Journal Article BCS Information Security Now (ISNow), 4 (2), pp. 6–7, 2009. Abstract | Links | BibTeX | Tags: @article{Papanikolaou2009a, title = {Security versus Quantum Computers}, author = {Nick Papanikolaou}, url = {../files/qcbcs.docx}, year = {2009}, date = {2009-01-01}, journal = {BCS Information Security Now (ISNow)}, volume = {4}, number = {2}, pages = {6--7}, abstract = {Quantum cryptography is all about achieving secure key distribution using the phenomena of quantum mechanics. It is now an implemented technology, and promises to work even when large scale quantum computers become widely available. In this article we will try to demystify quantum cryptography. As we will see, quantum cryptography relies on the same fundamental phenomena as a quantum computer, but its security is independent of an attacker's computational power and so is designed to be safe against such a device. The security of many classical cryptosystems such as RSA, on the other hand, is threatened by the very idea of a quantum computer.}, keywords = {}, pubstate = {published}, tppubtype = {article} } Quantum cryptography is all about achieving secure key distribution using the phenomena of quantum mechanics. It is now an implemented technology, and promises to work even when large scale quantum computers become widely available. In this article we will try to demystify quantum cryptography. As we will see, quantum cryptography relies on the same fundamental phenomena as a quantum computer, but its security is independent of an attacker's computational power and so is designed to be safe against such a device. The security of many classical cryptosystems such as RSA, on the other hand, is threatened by the very idea of a quantum computer. |
2008 |
|
| 14. | Davidson, Tim; Mlnařík, Hynek; Nagarajan, Rajagopal; Papanikolaou, Nikolaos Verifying Communicating Quantum Processes using QMC Technical Report Department of Computer Science, University of Warwick. 2008. BibTeX | Tags: @techreport{Davidson2008, title = {Verifying Communicating Quantum Processes using QMC}, author = {Tim Davidson and Hynek Mlnařík and Rajagopal Nagarajan and Nikolaos Papanikolaou}, year = {2008}, date = {2008-01-01}, institution = {Department of Computer Science, University of Warwick.}, keywords = {}, pubstate = {published}, tppubtype = {techreport} } |
| 13. | Gay, Simon; Nagarajan, Rajagopal; Papanikolaou, Nikolaos QMC: A Model Checker for Quantum Systems Inproceedings Proceedings of 20textsuperscriptth International Conference on Automated Verification (CAV 2008), Springer, Princeton, NJ, USA, 2008. Abstract | Links | BibTeX | Tags: @inproceedings{Gay2008, title = {QMC: A Model Checker for Quantum Systems}, author = {Simon Gay and Rajagopal Nagarajan and Nikolaos Papanikolaou}, url = {../files/gnp-cav.pdf}, year = {2008}, date = {2008-01-01}, booktitle = {Proceedings of 20textsuperscriptth International Conference on Automated Verification (CAV 2008)}, volume = {5123}, publisher = {Springer}, address = {Princeton, NJ, USA}, series = {Lecture Notes in Computer Science}, abstract = {We introduce a model-checking tool intended specially for the analysis of quantum information protocols. The tool incorporates an efficient representation of a certain class of quantum circuits, namely those expressible in the so-called stabiliser formalism. Models of protocols are described using a simple, imperative style simulation language which includes commands for the unitary operators in the Clifford group as well as classical integer and boolean variables. Formulas for verification are expressed using a subset of exogenous quantum propositional logic (EQPL). The model-checking procedure treats quantum measurements as the source of non-determinism, leading to multiple protocol runs, one for each outcome. Verification is performed for each run.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We introduce a model-checking tool intended specially for the analysis of quantum information protocols. The tool incorporates an efficient representation of a certain class of quantum circuits, namely those expressible in the so-called stabiliser formalism. Models of protocols are described using a simple, imperative style simulation language which includes commands for the unitary operators in the Clifford group as well as classical integer and boolean variables. Formulas for verification are expressed using a subset of exogenous quantum propositional logic (EQPL). The model-checking procedure treats quantum measurements as the source of non-determinism, leading to multiple protocol runs, one for each outcome. Verification is performed for each run. |
2007 |
|
| 12. | Gay, Simon; Nagarajan, Rajagopal; Papanikolaou, Nikolaos QMC: A Model Checker for Quantum Systems Inproceedings Proceedings of Workshop on Quantum Cryptography and Security (Lisbon Quantum Computation, Information and Logic Meetings Series: LQCIL'07), Lisbon, Portugal, 2007. Abstract | Links | BibTeX | Tags: @inproceedings{Gay2007, title = {QMC: A Model Checker for Quantum Systems}, author = {Simon Gay and Rajagopal Nagarajan and Nikolaos Papanikolaou}, url = {../files/gnp-lqcil.pdf}, year = {2007}, date = {2007-07-01}, booktitle = {Proceedings of Workshop on Quantum Cryptography and Security (Lisbon Quantum Computation, Information and Logic Meetings Series: LQCIL'07)}, address = {Lisbon, Portugal}, abstract = {We introduce a model-checking tool intended specially for the analysis of quantum information protocols. The tool incorporates an efficient representation of a certain class of quantum circuits, namely those expressible in the so-called stabiliser formalism. Models of protocols are described using a simple, imperative style simulation language which includes commands for the unitary operators in the Clifford group as well as classical integer and boolean variables. Formulas for verification are expressed using a subset of exogenous quantum propositional logic (EQPL). The model-checking procedure treats quantum measurements as the source of non-determinism, leading to multiple protocol runs, one for each outcome. Verification is performed for each run.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We introduce a model-checking tool intended specially for the analysis of quantum information protocols. The tool incorporates an efficient representation of a certain class of quantum circuits, namely those expressible in the so-called stabiliser formalism. Models of protocols are described using a simple, imperative style simulation language which includes commands for the unitary operators in the Clifford group as well as classical integer and boolean variables. Formulas for verification are expressed using a subset of exogenous quantum propositional logic (EQPL). The model-checking procedure treats quantum measurements as the source of non-determinism, leading to multiple protocol runs, one for each outcome. Verification is performed for each run. |
| 11. | Baltazar, Pedro; Mateus, Paulo; Nagarajan, Rajagopal; Papanikolaou, Nikolaos Exogenous Probabilistic Computation Tree Logic Inproceedings Proceedings of the Fifth Workshop on Quantitative Aspects of Programming Languages (QAPL '07), Braga, Portugal, 2007. Abstract | Links | BibTeX | Tags: @inproceedings{Baltazar2007, title = {Exogenous Probabilistic Computation Tree Logic}, author = {Pedro Baltazar and Paulo Mateus and Rajagopal Nagarajan and Nikolaos Papanikolaou}, url = {../files/qapl2007.pdf}, year = {2007}, date = {2007-01-01}, booktitle = {Proceedings of the Fifth Workshop on Quantitative Aspects of Programming Languages (QAPL '07)}, address = {Braga, Portugal}, abstract = {We define a logic EpCTL for reasoning about the evolution of probabilistic systems. System states correspond to probability distributions over classical states and the system evolution is modelled by probabilistic Kripke structures that capture both stochastic and non-deterministic transitions. The proposed logic is a temporal enrichment of Exogenous Probabilistic Propositional Logic (EPPL). The model-checking problem for EpCTL is analysed and the logic is compared with PCTL; the semantics of the former is defined in terms of probability distributions over sets of propositional symbols, whereas the latter is designed for reasoning about distributions over paths of possible behaviour. The intended application of the logic is as a specification formalism for properties of communication protocols, and security protocols in particular; to demonstrate this, we specify relevant security properties for a classical contract signing protocol and for the so-called quantum one-time pad.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We define a logic EpCTL for reasoning about the evolution of probabilistic systems. System states correspond to probability distributions over classical states and the system evolution is modelled by probabilistic Kripke structures that capture both stochastic and non-deterministic transitions. The proposed logic is a temporal enrichment of Exogenous Probabilistic Propositional Logic (EPPL). The model-checking problem for EpCTL is analysed and the logic is compared with PCTL; the semantics of the former is defined in terms of probability distributions over sets of propositional symbols, whereas the latter is designed for reasoning about distributions over paths of possible behaviour. The intended application of the logic is as a specification formalism for properties of communication protocols, and security protocols in particular; to demonstrate this, we specify relevant security properties for a classical contract signing protocol and for the so-called quantum one-time pad. |
2006 |
|
| 10. | Gay, Simon; Nagarajan, Rajagopal; Papanikolaou, Nikolaos Probabilistic Model-Checking of Quantum Protocols Inproceedings Proceedings of 2textsuperscriptnd International Workshop on Developments on Computational Models (DCM 2006), San Servolo, Venice, Italy, 2006. Abstract | Links | BibTeX | Tags: @inproceedings{Gay2006, title = {Probabilistic Model-Checking of Quantum Protocols}, author = {Simon Gay and Rajagopal Nagarajan and Nikolaos Papanikolaou}, url = {../files/dcmpaper.pdf}, year = {2006}, date = {2006-07-01}, booktitle = {Proceedings of 2textsuperscriptnd International Workshop on Developments on Computational Models (DCM 2006)}, address = {San Servolo, Venice, Italy}, abstract = {We establish fundamental and general techniques for formal verification of quantum protocols. Quantum protocols are novel communication schemes involving the use of quantum-mechanical phenomena for representation, storage and transmission of data. As opposed to quantum computers, quantum communication systems can and have been implemented using present-day technology; therefore, the ability to model and analyse such systems rigorously is of primary importance. While current analyses of quantum protocols use a traditional mathematical approach and require considerable understanding of the underlying physics, we argue that automated verification techniques provide an elegant alternative. We demonstrate these techniques through the use of PRISM, a probabilistic model-checking tool. Our approach is conceptually simpler than existing proofs, and allows us to disambiguate protocol definitions and assess their properties. It also facilitates detailed analyses of actual implemented systems. We illustrate our techniques by modelling a selection of quantum protocols (namely superdense coding, quantum teleportation, and quantum error correction) and verifying their basic correctness properties. Our results provide a foundation for further work on modelling and analysing larger systems such as those used for quantum cryptography, in which basic protocols are used as components.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We establish fundamental and general techniques for formal verification of quantum protocols. Quantum protocols are novel communication schemes involving the use of quantum-mechanical phenomena for representation, storage and transmission of data. As opposed to quantum computers, quantum communication systems can and have been implemented using present-day technology; therefore, the ability to model and analyse such systems rigorously is of primary importance. While current analyses of quantum protocols use a traditional mathematical approach and require considerable understanding of the underlying physics, we argue that automated verification techniques provide an elegant alternative. We demonstrate these techniques through the use of PRISM, a probabilistic model-checking tool. Our approach is conceptually simpler than existing proofs, and allows us to disambiguate protocol definitions and assess their properties. It also facilitates detailed analyses of actual implemented systems. We illustrate our techniques by modelling a selection of quantum protocols (namely superdense coding, quantum teleportation, and quantum error correction) and verifying their basic correctness properties. Our results provide a foundation for further work on modelling and analysing larger systems such as those used for quantum cryptography, in which basic protocols are used as components. |
| 9. | Papanikolaou, Nikolaos; Nagarajan, Rajagopal Classical Security Protocols for QKD Systems Technical Report EU FP6 SECOQC Project 2006. Abstract | Links | BibTeX | Tags: @techreport{Papanikolaou2006, title = {Classical Security Protocols for QKD Systems}, author = {Nikolaos Papanikolaou and Rajagopal Nagarajan}, url = {../files/protocols.pdf}, year = {2006}, date = {2006-01-01}, institution = {EU FP6 SECOQC Project}, abstract = {The purpose of this report is to document the three principal classes of classic cryptographic protocols which are needed in systems for quantum key distribution. We will detail the protocols used for secret-key reconciliation by public discussion, privacy amplification by public discussion, and unconditionally secure authentication. We suggest the use of the model checking method for the analysis of these protocols and the verification of relevant security requirements; the model checking technique is described, and the PRISM model checker is presented.}, keywords = {}, pubstate = {published}, tppubtype = {techreport} } The purpose of this report is to document the three principal classes of classic cryptographic protocols which are needed in systems for quantum key distribution. We will detail the protocols used for secret-key reconciliation by public discussion, privacy amplification by public discussion, and unconditionally secure authentication. We suggest the use of the model checking method for the analysis of these protocols and the verification of relevant security requirements; the model checking technique is described, and the PRISM model checker is presented. |
2005 |
|
| 8. | Nagarajan, Rajagopal; Papanikolaou, Nikolaos; Bowen, Garry; Gay, Simon An Automated Analysis of the Security of Quantum Key Distribution Inproceedings Proceedings of the Third International Workshop on Security Issues in Concurrency (SECCO'05), San Francisco, USA, 2005. Abstract | Links | BibTeX | Tags: @inproceedings{Nagarajan2005, title = {An Automated Analysis of the Security of Quantum Key Distribution}, author = {Rajagopal Nagarajan and Nikolaos Papanikolaou and Garry Bowen and Simon Gay}, url = {../files/NRG-secco05.pdf}, year = {2005}, date = {2005-08-01}, booktitle = {Proceedings of the Third International Workshop on Security Issues in Concurrency (SECCO'05)}, address = {San Francisco, USA}, abstract = {This paper discusses the use of computer--aided verification as a practical means for analysing quantum information systems; specifically, the BB84 protocol for quantum key distribution is examined using this method. This protocol has been shown to be unconditionally secure against all attacks in an information--theoretic setting, but the relevant security proof requires a thorough understanding of the formalism of quantum mechanics and is not easily adaptable to practical scenarios. Our approach is based on probabilistic model--checking; we have used the PRISM model--checker to show that, as the number of qubits transmitted in BB84 is increased, the amount of valid information held by an eavesdropper about the transmitted key decreases exponentially. We have also shown that the probability of detecting the presence of an eavesdropper increases exponentially with the number of qubits. Our results demonstrate the effectiveness of the model--checking approach for systems where analytical solutions may not be possible or plausible.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } This paper discusses the use of computer--aided verification as a practical means for analysing quantum information systems; specifically, the BB84 protocol for quantum key distribution is examined using this method. This protocol has been shown to be unconditionally secure against all attacks in an information--theoretic setting, but the relevant security proof requires a thorough understanding of the formalism of quantum mechanics and is not easily adaptable to practical scenarios. Our approach is based on probabilistic model--checking; we have used the PRISM model--checker to show that, as the number of qubits transmitted in BB84 is increased, the amount of valid information held by an eavesdropper about the transmitted key decreases exponentially. We have also shown that the probability of detecting the presence of an eavesdropper increases exponentially with the number of qubits. Our results demonstrate the effectiveness of the model--checking approach for systems where analytical solutions may not be possible or plausible. |
| 7. | Nagarajan, Rajagopal; Papanikolaou, Nikolaos; Williams, David Simulating and Compiling Code for the Sequential Quantum Random Access Machine Inproceedings Proceedings of the Third International Workshop on Quantum Programming Languages (QPL 2005), pp. 101–124, DePaul University, Chicago, USA, 2005. Abstract | Links | BibTeX | Tags: @inproceedings{Nagarajan2005a, title = {Simulating and Compiling Code for the Sequential Quantum Random Access Machine}, author = {Rajagopal Nagarajan and Nikolaos Papanikolaou and David Williams}, url = {../files/qpl05.pdf}, year = {2005}, date = {2005-07-01}, booktitle = {Proceedings of the Third International Workshop on Quantum Programming Languages (QPL 2005)}, volume = {170}, pages = {101--124}, address = {DePaul University, Chicago, USA}, series = {Electronic Notes in Theoretical Computer Science}, abstract = {We present the SQRAM architecture for quantum computing, which is based on Knill's QRAM model. We detail a suitable instruction set, which implements a universal set of quantum gates, and demonstrate the operation of the SQRAM with Deutsch's quantum algorithm. The compilation of high-level quantum programs for the SQRAM machine is considered; we present templates for quantum assembly code and a method for decomposing matrices for complex quantum operations. The SQRAM simulator and compiler are discussed, along with directions for future work.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } We present the SQRAM architecture for quantum computing, which is based on Knill's QRAM model. We detail a suitable instruction set, which implements a universal set of quantum gates, and demonstrate the operation of the SQRAM with Deutsch's quantum algorithm. The compilation of high-level quantum programs for the SQRAM machine is considered; we present templates for quantum assembly code and a method for decomposing matrices for complex quantum operations. The SQRAM simulator and compiler are discussed, along with directions for future work. |
| 6. | Papanikolaou, Nick An Introduction to Quantum Cryptography Journal Article ACM Crossroads, 11 (3), pp. 10–16, 2005, (Also available at http://www.xrds.org.). Abstract | Links | BibTeX | Tags: @article{Papanikolaou2005, title = {An Introduction to Quantum Cryptography}, author = {Nick Papanikolaou}, url = {../files/qcryp.htm}, year = {2005}, date = {2005-01-01}, journal = {ACM Crossroads}, volume = {11}, number = {3}, pages = {10--16}, abstract = {This paper is a frequently cited introduction to the topic of quantum cryptography.}, note = {Also available at http://www.xrds.org.}, keywords = {}, pubstate = {published}, tppubtype = {article} } This paper is a frequently cited introduction to the topic of quantum cryptography. |
| 5. | Papanikolaou, Nick Reasoning Formally About Quantum Systems: An Overview Journal Article ACM SIGACT News, 36 (3), pp. 51–66, 2005. Abstract | Links | BibTeX | Tags: @article{Papanikolaou2005a, title = {Reasoning Formally About Quantum Systems: An Overview}, author = {Nick Papanikolaou}, url = {../files/qsurvey.pdf}, year = {2005}, date = {2005-01-01}, journal = {ACM SIGACT News}, volume = {36}, number = {3}, pages = {51--66}, abstract = {This article is intended as an introduction to the subject of quantum logic, and as a brief survey of the relevant literature. Also discussed here are logics for specification and analysis of quantum information systems, in particular, recent work by P. Mateus and A. Sernadas, and also by R. van der Meyden and M. Patra. Overall, the objective is to provide a high-level presentation of the logical aspects of quantum theory.}, keywords = {}, pubstate = {published}, tppubtype = {article} } This article is intended as an introduction to the subject of quantum logic, and as a brief survey of the relevant literature. Also discussed here are logics for specification and analysis of quantum information systems, in particular, recent work by P. Mateus and A. Sernadas, and also by R. van der Meyden and M. Patra. Overall, the objective is to provide a high-level presentation of the logical aspects of quantum theory. |
| 4. | Papanikolaou, Nick Review of Classical and Quantum Computing by Yorick Hardy and Willi-Hans Steeb, Birkhauser Verlag, 2001 (ISBN: 3-7643-6610-9) Journal Article ACM SIGACT News, 36 (3), pp. 5–9, 2005. @article{Papanikolaou2005b, title = {Review of Classical and Quantum Computing by Yorick Hardy and Willi-Hans Steeb, Birkhauser Verlag, 2001 (ISBN: 3-7643-6610-9)}, author = {Nick Papanikolaou}, url = {../files/bookreviewhsteeb.pdf}, year = {2005}, date = {2005-01-01}, journal = {ACM SIGACT News}, volume = {36}, number = {3}, pages = {5--9}, keywords = {}, pubstate = {published}, tppubtype = {article} } |
| 3. | Papanikolaou, Nick Review of Data Privacy and Security by David Salomon, Springer-Verlag, 2003 (ISBN: 0-387-00311-8) Journal Article ACM SIGACT News, 36 (2), pp. 8–13, 2005. @article{Papanikolaou2005c, title = {Review of Data Privacy and Security by David Salomon, Springer-Verlag, 2003 (ISBN: 0-387-00311-8)}, author = {Nick Papanikolaou}, url = {../files/bookreviewsalomon.pdf}, year = {2005}, date = {2005-01-01}, journal = {ACM SIGACT News}, volume = {36}, number = {2}, pages = {8--13}, keywords = {}, pubstate = {published}, tppubtype = {article} } |
2004 |
|
| 2. | Papanikolaou, Nikolaos A Programming Language for Quantum Communication Systems Design Inproceedings Proceedings of the IEEE Postgraduate Research in Electronics, Photonics, Communications and Software Conference (PREP2004), University of Hertfordshire, United Kingdom, 2004. Abstract | Links | BibTeX | Tags: @inproceedings{Papanikolaou2004, title = {A Programming Language for Quantum Communication Systems Design}, author = {Nikolaos Papanikolaou}, url = {../files/prepabstract.pdf}, year = {2004}, date = {2004-01-01}, booktitle = {Proceedings of the IEEE Postgraduate Research in Electronics, Photonics, Communications and Software Conference (PREP2004)}, address = {University of Hertfordshire, United Kingdom}, abstract = {Several languages for quantum programming have been proposed before, which facilitate the description of algorithms for quantum computers. None such language has been developed specifically for protocol design and validation. Protocols for quantum cryptography give a guarantee of immunity to eavesdropping, but proofs of their unconditional security are purely theoretical. The goal of this work is to establish a framework for formal definition and validation of quantum protocols.}, keywords = {}, pubstate = {published}, tppubtype = {inproceedings} } Several languages for quantum programming have been proposed before, which facilitate the description of algorithms for quantum computers. None such language has been developed specifically for protocol design and validation. Protocols for quantum cryptography give a guarantee of immunity to eavesdropping, but proofs of their unconditional security are purely theoretical. The goal of this work is to establish a framework for formal definition and validation of quantum protocols. |
| 1. | Papanikolaou, Nikolaos Techniques for Design and Validation of Quantum Protocols Masters Thesis Department of Computer Science, University of Warwick, 2004. Abstract | Links | BibTeX | Tags: @mastersthesis{Papanikolaou2004a, title = {Techniques for Design and Validation of Quantum Protocols}, author = {Nikolaos Papanikolaou}, url = {../files/nmsc.pdf}, year = {2004}, date = {2004-01-01}, school = {Department of Computer Science, University of Warwick}, 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.}, keywords = {}, pubstate = {published}, tppubtype = {mastersthesis} } 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. |
List of Publications
2009 |
|
| 17. | Towards an Integrated Approach to the Management, Specification and Enforcement of Privacy Policies Inproceedings Proceedings of W3C Workshop on Access Control Application Scenarios, Abbaye de Neumünster, Luxembourg, 2009. |
| 16. | Model Checking Quantum Protocols PhD Thesis Department of Computer Science, University of Warwick, 2009. |
| 15. | Security versus Quantum Computers Journal Article BCS Information Security Now (ISNow), 4 (2), pp. 6–7, 2009. |
2008 |
|
| 14. | Verifying Communicating Quantum Processes using QMC Technical Report Department of Computer Science, University of Warwick. 2008. |
| 13. | QMC: A Model Checker for Quantum Systems Inproceedings Proceedings of 20textsuperscriptth International Conference on Automated Verification (CAV 2008), Springer, Princeton, NJ, USA, 2008. |
2007 |
|
| 12. | QMC: A Model Checker for Quantum Systems Inproceedings Proceedings of Workshop on Quantum Cryptography and Security (Lisbon Quantum Computation, Information and Logic Meetings Series: LQCIL'07), Lisbon, Portugal, 2007. |
| 11. | Exogenous Probabilistic Computation Tree Logic Inproceedings Proceedings of the Fifth Workshop on Quantitative Aspects of Programming Languages (QAPL '07), Braga, Portugal, 2007. |
2006 |
|
| 10. | Probabilistic Model-Checking of Quantum Protocols Inproceedings Proceedings of 2textsuperscriptnd International Workshop on Developments on Computational Models (DCM 2006), San Servolo, Venice, Italy, 2006. |
| 9. | Classical Security Protocols for QKD Systems Technical Report EU FP6 SECOQC Project 2006. |
2005 |
|
| 8. | An Automated Analysis of the Security of Quantum Key Distribution Inproceedings Proceedings of the Third International Workshop on Security Issues in Concurrency (SECCO'05), San Francisco, USA, 2005. |
| 7. | Simulating and Compiling Code for the Sequential Quantum Random Access Machine Inproceedings Proceedings of the Third International Workshop on Quantum Programming Languages (QPL 2005), pp. 101–124, DePaul University, Chicago, USA, 2005. |
| 6. | An Introduction to Quantum Cryptography Journal Article ACM Crossroads, 11 (3), pp. 10–16, 2005, (Also available at http://www.xrds.org.). |
| 5. | Reasoning Formally About Quantum Systems: An Overview Journal Article ACM SIGACT News, 36 (3), pp. 51–66, 2005. |
| 4. | Review of Classical and Quantum Computing by Yorick Hardy and Willi-Hans Steeb, Birkhauser Verlag, 2001 (ISBN: 3-7643-6610-9) Journal Article ACM SIGACT News, 36 (3), pp. 5–9, 2005. |
| 3. | Review of Data Privacy and Security by David Salomon, Springer-Verlag, 2003 (ISBN: 0-387-00311-8) Journal Article ACM SIGACT News, 36 (2), pp. 8–13, 2005. |
2004 |
|
| 2. | A Programming Language for Quantum Communication Systems Design Inproceedings Proceedings of the IEEE Postgraduate Research in Electronics, Photonics, Communications and Software Conference (PREP2004), University of Hertfordshire, United Kingdom, 2004. |
| 1. | Techniques for Design and Validation of Quantum Protocols Masters Thesis Department of Computer Science, University of Warwick, 2004. |