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
In: 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.
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.
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
In: 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.
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
In: 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.
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
In: 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.
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
In: 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.
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
In: 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.
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.
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
In: 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.
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
In: 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.
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
In: 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.
cryptography.
5.
Papanikolaou, Nick
Reasoning Formally About Quantum Systems: An Overview Journal Article
In: 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.
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
In: 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
In: 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
In: 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.
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.
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.