Dr Nick Papanikolaou
Welcome
You are now looking at Nick Papanikolaou's personal webpage. The purpose of the site is to provide information on Nick's professional
activities and research.
Nick is a Researcher in the Cloud and Security Lab
at Hewlett-Packard Laboratories (HP
Labs), Bristol. He is currently involved in Future Internet Research in the areas of trust and security, particularly with applications in cloud computing.
Previously, Nick was Research Fellow in the
e-Security Group at the
International Digital Laboratory
within the University of Warwick (part of
the WMG institute), working
in collaboration with Sadie Creese and Michael Goldsmith. In
that role he worked on mathematical models of privacy, specification languages and
models of policies, and design and verification of security protocols as part of
the project EnCoRe ("Ensuring Consent
and Revocation"). During his doctorate, he was employed on a part-time basis by Resource
Development International (RDI), as "Pathway Leader" and Tutor for the HND/C Computing (Business
IT) distance learning course, and Tutor for the BA in Business IT Topup
course. RDI provides these programmes to business clients and independent
students. Nick studied computer science at the University of
Warwick, completing a BSc (Hons) in Computer Systems Engineering, an
MSc by Research, and a PhD in Computer Science. His doctorate was supervised by
Rajagopal Nagarajan.
Nick is a member of the Association for Computing Machinery (ACM),
the Institute for Electrical and Electronic Engineers (IEEE)
and the European Research Consortium for Informatics and Mathematics (ERCIM).
He is a member of the ACM Special Interest Group on Algorithms and Computation
Theory (SIGACT), the ACM Special Interest
Group on Programming Languages (SIGPLAN),
the IEEE Computer Society and the
European Association for Theoretical Computer Science (EATCS).
He actively presents research at workshops and conferences in
theoretical computer science and computer security and has served on various programme committees; Nick was also on the organising committee of the Fifth Workshop on Automated
Verification of Critical Systems (AVoCS'05).
Nick has received two awards:
- Computer Systems Engineering Project Prize, Department of Computer
Science, University of Warwick, 2003.
- Best Presentation Award,
WPCCS'06 (Warwick Postgraduate Colloquium on Computer Science),
Department of Computer Science, University of Warwick, 2006.
At the University of Warwick, Nick was a teaching assistant for several course modules
in the Department of Computer Science, including among others
the courses CS134 (Introduction to Computer Security), CS238
(Concurrent Processes) and
CS406 (Research
Directions in Computing).
As of March 2011, Nick is a trained and Certified ScrumMaster and Member of the Scrum Alliance.
In May 2011 he was granted the honorary title of Associate Fellow by the
Department of Computer Science at
the University of Warwick.
Research
Interests:
- cloud security and privacy
- policy formalisation and enforcement
- natural language processing, applied AI
- model checking and process algebra
- quantum cryptography
Some Past Results and Contributions:
- Design of languages, logics and tools for protocol specification and
verification
- In joint work with
Paulo Mateus and
Pedro Baltazar (IST Lisbon), Nick helped to
develop EpCTL, a probabilistic temporal
logic that uses EPPL (exogenous probabilistic propositional logic) as
its core.
- Model checking
- In collaboration with Rajagopal Nagarajan
and Simon Gay Nick
developed a model checker, QMC, for the analysis of properties of
quantum communication and quantum cryptographic protocols. QMC is the
first of its kind to my knowledge. Earlier work has included the use of
a classical, probabilistic model checker for the analysis of similar
protocols. This work combined classical verification
techniques and models with the mathematics of quantum computing and
quantum information, so this is clearly interdisciplinary.
- Syntax and semantics of languages for quantum programming
- Nick's undergraduate final year project 'Formal Specification and
Verification of Quantum Protocols' extended the work of Simon Gay and Rajagopal Nagarajan on verifying the security of the BB84 protocol using classical
process algebra and the probabilistic model checker
PRISM. He was involved in
the early stages of development of CQP (Communicating Quantum
Processes), a quantum process algebra with a formal semantics and
type system. Nick developed a quantum
specification language for use in conjunction with the QMC model
checker; the language has an operational semantics and an
implementation.
Research Projects
Nick has been involved in the following research projects.
Publications
For an alternative listing of publications see Nick's
HP Labs page and
also my (not complete)
DBLP entries.
Below this listing of papers by year you will also find Nick's:
2011
Nick Papanikolaou, Siani Pearson, and Marco Casassa Mont. Towards Natural-Language Understanding and
Automated Enforcement of Privacy Rules and Regulations in the Cloud: Survey and Bibliography. Accepted for publication in Proceedings of 1st International Workshop on Security and Trust in Virtualised Environments (STAVE 2011).- Nikolaos Papanikolaou, Sadie Creese, and Michael Goldsmith. Refinement Checking for Privacy Policies. Science of Computer Programming. Accepted for publication - to appear 2011.
- T. Davidson, S. J. Gay, H. Mlnarik, R. Nagarajan and N. Papanikolaou. Model Checking for Communicating Quantum Processes. International Journal of Unconventional Computing. Accepted for publication - to appear 2011.
2010
- Marco Casassa Mont, Siani Pearson, Sadie Creese, Michael Goldsmith, and
Nick Papanikolaou. A Conceptual Model for Privacy Policies with Consent
and Revocation Requirements. In Proceedings of PrimeLife/IFIP Summer
School 2010: Privacy and Identity Management for Life, Lecture Notes in
Computer Science, Springer-Verlag 2010.
- Adedayo O. Adetoye and Nikolaos Papanikolaou, Static Analysis of
Information Release in Interactive Programs. In Proceedings of 10th
International Workshop on Automated Verification of Critical Systems (AVoCS
'10), Dusseldorf, Germany, September 20-23, 2010.
- Ioannis Agrafiotis, Sadie Creese, Michael Goldsmith, and Nick
Papanikolaou. Applying Formal Methods to Describe Privacy Control
Requirements in a Real Scenario: Emerging Ambiguities and Proposed
Solutions. In Pre-Proceedings of PrimeLife/IFIP Summer School 2010:
Privacy and Identity Management for Life, Helsingborg, Sweden, August
2010.
- Ioannis Agrafiotis, Sadie Creese, Michael Goldsmith, Nick Papanikolaou,
Marco Casassa Mont, and Siani Pearson. Defining consent and revocation
policies. In Pre-Proceedings of PrimeLife/IFIP Summer School 2010:
Privacy and Identity Management for Life, Helsingborg, Sweden, August
2010.
- Marco Casassa Mont, Siani Pearson, Sadie Creese, Michael Goldsmith, and
Nick Papanikolaou. EnCoRe: Towards a conceptual model for privacy
policies. In Pre-Proceedings of PrimeLife/IFIP Summer School 2010:
Privacy and Identity Management for Life, Helsingborg, Sweden, August
2010.
- Nick Papanikolaou, Sadie Creese, Michael Goldsmith, Marco Casassa Mont,
and Siani Pearson. EnCoRe: Towards a holistic approach to privacy. In
Proceedings of International Conference on Security and Cryptography
(SECRYPT 2010), Athens, Greece, July 2010.
- Nick Papanikolaou. Security versus quantum computers. BCS
Information Security Now (ISNow), 4(2):6-7, Winter 2009/10.
- S. J. Gay, R. Nagarajan and N. Papanikolaou. 'Specification and
Verification of Quantum Protocols'. Chapter 11 of Semantic Techniques
in Quantum Computation, S.J. Gay and I. Mackie (eds.). Cambridge
University Press, 2010.
2009
- Marco Casassa Mont, Siani Pearson, Sadie Creese, Michael Goldsmith, and
Nick Papanikolaou. Towards an integrated approach to the management,
specification and enforcement of privacy policies. In Proceedings of
W3C Workshop on Access Control Application Scenarios, Abbaye de
Neumunster, Luxembourg, November 2009.
- Ioannis Agrafiotis, Sadie Creese, Michael Goldsmith, and Nikolaos
Papanikolaou. Reaching for informed revocation: Shutting off the tap on
personal data. In Proceedings of Fifth International Summer School on
Privacy and Identity Management for Life, Nice, France, September 2009.
- Nikolaos Papanikolaou, Sadie Creese, and Michael Goldsmith. Policy
refinement checking (extended abstract). In Proceedings of Ninth
International Workshop on Automated Verification of Critical Systems (AVoCS
09), Swansea University, September 2009.
2008
- Simon Gay, Rajagopal Nagarajan, and Nikolaos Papanikolaou. QMC: A
model checker for quantum systems. In Proceedings of 20th
International Conference on Automated Verification (CAV 2008), volume
5123 of Lecture Notes in Computer Science, Princeton, NJ, USA, July
2008. Springer.
2007
- Simon Gay, Rajagopal Nagarajan, and Nikolaos Papanikolaou. QMC: A
model checker for quantum systems. In Proceedings of Workshop on
Quantum Cryptography and Security (Lisbon Quantum Computation, Information
and Logic Meetings Series: LQCIL'07), Lisbon, Portugal, July 2007.
- Pedro Baltazar, Paulo Mateus, Rajagopal Nagarajan, and Nikolaos
Papanikolaou. Exogenous probabilistic computation tree logic. In
Proceedings of the Fifth Workshop on Quantitative Aspects of Programming
Languages (QAPL '07), Braga, Portugal, March 2007.
2006
- Simon Gay, Rajagopal Nagarajan, and Nikolaos Papanikolaou.
Probabilistic model-checking of quantum protocols. In Proceedings of
2nd International Workshop on Developments on Computational Models (DCM
2006), 2006.
- Extended abstract: pdf
- Pre-proceedings version: pdf
2005
- Nick Papanikolaou. Reasoning formally about quantum systems: An
overview. ACM SIGACT News, 36(3):51-66, 2005.
- Departmental Research Report
CS-RR-416, Department of Computer Science, University of Warwick.
- arXiv version - cs.LO/0508005:
link.
- Rajagopal Nagarajan, Nikolaos Papanikolaou, Garry Bowen, and Simon Gay.
An automated analysis of the security of quantum key distribution. In
Proceedings of the Third International Workshop on Security Issues in
Concurrency (SECCO'05), San Francisco, USA, August 2005.
- Rajagopal Nagarajan, Nikolaos Papanikolaou, and David Williams. Simulating and compiling code for the sequential quantum random access
machine. In Proceedings of the Third International Workshop on
Quantum Programming Languages (QPL 2005), volume 170 of Electronic Notes
in Theoretical Computer Science, pages 101-124, DePaul University, Chicago,
USA, 2005.
- N. Papanikolaou. An introduction to quantum cryptography. ACM
Crossroads, 11(3):10-16, 2005.
- Online version available
here.
2004
- N. Papanikolaou. A programming language for quantum communication
systems design. In Proceedings of the IEEE PREP2004 Conference,
University of Hertfordshire, United Kingdom, 2004.
Theses
- N. Papanikolaou. Model Checking Quantum Protocols. Ph.D. Thesis,
Department of Computer Science, University of Warwick, 2009.
- Available as
pdf [1,191 KB].
- N. Papanikolaou. Techniques for Design and Validation of Quantum
Protocols. M.Sc. Thesis, Department of Computer Science, University of
Warwick, 2004.
- Available as
pdf [607 KB].
- Also available as Research Thesis CS-RT-413
here.
- N. Papanikolaou. Formal Specification and Verification of Quantum
Cryptographic Protocols. Undergraduate Computing Project Report/B.Sc.
Thesis, Department of Computer Science, University of Warwick, 2003.
- Available as
pdf
[511 KB].
Book Reviews
- Book Review of 'Algorithms and Theory of Computation Handbook'
Vols I and II, Edited by : Mikhail J. Atallah and Marina Blanton, Chapman &
Hall / CRC Press, 2010 (ISBN: 978-1-58488-822-2).
- Book Review of 'The Space and Motion of Communicating Agents' by
Robin Milner, Cambridge University Press, 2009 (ISBN: 978-0-521-73833-0),
ACM SIGACT News,
41(3), 2010
- Available as
pdf [100 KB].
- Book Review of 'Data Privacy and Security' by David Salomon,
Springer-Verlag, 2003 (ISBN: 0-387-00311-8),
ACM SIGACT News,
36(2), pp. 8-13, 2005.
- Available as
pdf [107 KB].
- Book Review of 'Classical and Quantum Computing' by Yorick Hardy
and Willi-Hans Steeb, Birkhauser Verlag, 2001 (ISBN: 3-7643-6610-9),
ACM SIGACT News,
36(3), pp. 5-9, 2005 [pdf
[65 KB] ].
Technical Reports & Other Published Material
Technical Reports
- Marco Casassa Mont, Siani Pearson, Sadie Creese, Michael Goldsmith, Nick
Papanikolaou. Towards A Conceptual Model For Privacy Policies. HP
Labs Technical Report HPL-2010-82.
- Nick Papanikolaou, Sadie Creese, Michael Goldsmith, Marco Casassa Mont,
Siani Pearson. EnCoRe: Towards a holistic approach to privacy. HP
Labs Technical Report HPL-2010-83.
Special Contributions
- Write-up of my contribution to discussion following the BCS
Computer Journal Lecture "Quantum Information Flow: A Computer Science
Perspective" by Samson Abramsky (12/06/2007).
- Available as
pdf
[30 KB] .
Miscellaneous
- Tim Davidson, Hynek Mlnarik, Rajagopal Nagarajan, and Nikolaos
Papanikolaou. Verifying Communicating Quantum Processes using QMC.
2008.
- N. Papanikolaou. Definition of the QMC Specification Language
(Syntax and Operational Semantics).
- Nikolaos Papanikolaou, Rajagopal Nagarajan. Classical Security
Protocols for QKD Systems. 2006.
- Draft available as
pdf [207 KB].
- Simon Gay, Rajagopal Nagarajan, Nikolaos Papanikolaou. Probabilistic
Model-Checking of Quantum Protocols. 2005.
- Available as
pdf [238 KB].
Selected Talks
- "Defining Consent and Revocation Policies". Talk given at
PrimeLife/IFIP Summer School 2010, 2-6 August 2010, Helsingborg, Sweden.
- "Towards a Conceptual Model for Privacy Policies". Talk given at
PrimeLife/IFIP Summer School 2010, 2-6 August 2010, Helsingborg, Sweden.
- "Automated Search for Quantum Secret Sharing Protocols with Graph
States". Talk given at the Third QNET Workshop 2009 on Semantics of
Quantum Computation, 11 December 2009, School of Informatics, University of
Edinburgh, Scotland.
- "Towards Integrated Policy Management for Privacy". Talk given at
W3C Workshop on Access Control Application Scenarios, 17th November 2009,
Abbaye de Neumunster, Luxembourg.
- "Policy Refinement Checking." Talk given at Ninth International
Workshop on Automated Verification of Critical Systems (AVoCS 09), 23-25
September 2009, Swansea University, Wales, England.
- "Potential and Limitations of Quantum Key Distribution: An Introduction".
Invited talk at British Computer Society, 17 September 2009, as part
of BCS Security Strategic Panel on "The Future of
Cryptography".
- "Making Online Security Risks More Tangible". Talk given at Web
Science Conference 2009: Society Online, March 18-20, 2009, Foundation of
the Hellenic World, Athens, Greece.
- "Ensuring Consent and Revocation: Towards a Taxonomy of Consent".
Seminar (Concurrency, Verification and Security Seminar Series), February
11, 2009, Computing Laboratory, University of Oxford, Oxford, England.
- "Ensuring Consent and Revocation: Towards a Taxonomy of Consent".
Seminar (Digital Lab Seminar Series), February 4, 2009, International
Digital Laboratory, University of Warwick, Coventry, England. .
- "Verifying Quantum Secret Sharing Protocols with the Quantum Model
Checker." Talk given at the Second QNET Workshop, December 18-19, 2008,
School of Informatics, University of Edinburgh, Edinburgh, Scotland.
- "Model Checking a Quantum Protocol: Theory, Implementation and
Issues." Talk given at the First QNET Workshop, December 10-11, 2007,
The Royal Society, London, England.
- "QMC: A Model Checker for Quantum Systems." Talk given at 5th
Warwick Postgraduate Colloquium on Computer Science (WPCCS'07), July 3,
2007, Department of Computer Science, University of Warwick, Coventry,
England.
- Received Best Presentation Award (and cash prize)
- Slides available here
- "QMC: A Model Checker for Quantum Systems." Invited talk given at
Central European Quantum Information Processing Workshop (CEQIP'07), June
26, 2007, Valtice, Czech Republic.
- "On Model-Checking Exogenous Quantum Logic: Complexity Aspects and
Implementation." Algorithms and Formal Methods Seminar, January 29th,
2007, Department of Computer Science, University of Warwick, Coventry,
England.
- "Model Checking Quantum Stabilizer Protocols." Talk given at QNET
Workshop 2006 / Qday III, December 4th, 2006, University of Glasgow,
Glasgow, Scotland.
- "Towards a Model Checker for Quantum Stabilizer Protocols."
Seminar
given at Centro de Logica e Computacao / SQIG, November 17th, 2006,
Instituto Superior Tecnico, Lisbon, Portugal.
- "Towards a Verification Tool for Quantum Communication Protocols."
Talk given at Scottish Theorem Proving Seminar, June 6th, 2006,
University of Glasgow, Glasgow, Scotland.
- This talk was supported by
SymNet.
- "A Framework for Automated Verification of Quantum Cryptographic
Protocols." Talk given at BCTCS'06, April 5th, 2006, University of
Swansea, Wales, England.
- "Model-Checking Quantum Key Distribution: Techniques and Results."
Q-Day II Workshop on Mathematical Structures in Quantum Informatics,
December 8th, 2005, Institut Henri Poincare, Universite Pierre et Marie
Curie, Paris, France.
- "An Automated Analysis of the Security of Quantum Key
Distribution." AVoCS'05 Workshop, September 13th, 2005, University
of Warwick, Coventry, England.
- "An Automated Analysis of the Security of Quantum Key
Distribution." SecCo 2005, August 22, 2005, Stanford Court Hotel,
San Francisco, California, USA.
- "Introduction to Quantum Cryptography." Lecture, CS406 Research
Directions in Computing course, October 2004, Department of Computer
Science, University of Warwick, Coventry, England.
- "Quantum Gates and Circuits." Lecture, CS406 Research Directions
in Computing course, October 2004, Department of Computer Science,
University of Warwick, Coventry, England.
- "Basics of Quantum Computation." Lecture, CS406 Research
Directions in Computing course, October 2004, Department of Computer
Science, University of Warwick, Coventry, England.
- "Introduction to Quantum Cryptography." Lecture, CS406 Research
Directions in Computing course, October 2003, Department of Computer
Science, University of Warwick, Coventry, England.
- "Introduction to Quantum Computation and Quantum Information."
Open Day Presentation, October 2003, University of Warwick, Coventry,
England.
Software
Quantum Model Checker (QMC)
This section is devoted to the software Nick developed as part of his PhD, namely, the Quantum Model Checker (QMC). You will
find here a description of the tool and:
QMC is a tool that automatically explores all possible behaviours
arising from a quantum protocol description expressed in QMCLANG and enables
QCTL properties to be checked over the resulting structure. Quantum
protocols include only Clifford group operations on stabilizer states.
The QMC tool has three main components: (1) a process scheduler, (2) a
language interpreter, and (3) a model checker. The role of component (1) is
essentially to perform the tasks described in the previous paragraph. The
language interpreter handles the execution of individual commands and keeps
track of the overall classical and quantum state at each step. Finally, the
verifier is responsible for evaluating QCTL formulae over the structure
generated by (1) and (2). QMC has a graphical user interface which includes
a user–friendly editor for models and properties.
A protocol model consists of definitions of one or more processes. The
commands performed by these processes are interleaved, in order to simulate
concurrent execution. Nondeterministic choices are resolved in all possible
ways, producing a tree of all possible executions of the protocol.
QMC provides an interface to the
GraphViz graph layout tool,
and the
ZGRVIEWER application, which can display the program execution tree.
Given a model and a QCTL formula for verification, QMC outputs the following:
- a summary of the files provided as input and basic feedback on the model
provided including the number of states and the total number of runs,
- a verification result for the formula provided,
- a list of states (if any) that serve as counter-examples to the formula,
- a prompt which allows the user to track individual states and trace runs
of interest, as well as to verify further formulae.
Teaching
Nick's teaching at the University of Warwick (before moving to HP) has included
lectures for
CS406 Research Directions in Computing and
seminars for
CS134 Introduction to Computer Security.
Nick was Teaching Assistant to
Rajagopal
Nagarajan for the 4th year module
CS406
Research Directions in Computing. He taught a lecture-based mini-course on Lexical and Syntactic
Analysis as part of the 2nd year module
CS245 Automata and Formal Languages (academic years 2005-6, 2006-7, 2007-8,
2008-9). Lecture notes are available below.
Nick would give a yearly Guest Lecture on Quantum Cryptography for the
1st year module
CS134 Introduction to Computer Security (course organiser:
Jane Sinclair).
Nick was Teaching Assistant to
Sara Kalvala for
the 2nd year module
CS238 Concurrent Processes during the academic years 2003-2004 and
2004-2005.
Also, he assisted in surgery classes for CS120 Programming Laboratory during
the academic year 2003-2004 and was involved in providing feedback and marking
coursework for CS237 Concurrent Programming during the academic year
2003-2004.
More information and course notes are available below.
Seminars for CS134
Course materials for CS134 including seminar handouts are available
here (Warwick campus access only).
Lectures for CS406 (Lecture Notes below)
Handouts and Slides for Lectures and
Seminars
- CS134 (Introduction to Computer Security) Guest Lecture on
Quantum Cryptography [2007-8 version]
pdf [446 KB]
- CS245 (Automata and Formal Languages) Lecture 1 (31/01/2008) -
Lexical Analysis. Slides (2-3 per page)
pdf
[112 KB]
- CS245 (Automata and Formal Languages) Lecture 2 (01/02/2008)-
Top-Down Parsing. Slides (2-3 per page):
pdf
[111 KB]
- CS245 (Automata and Formal Languages) Lecture 3 (04/02/2008)-
Bottom-Up Parsing. Slides (2-3 per page):
pdf
[97 KB]
- CS238 (Concurrent Processes) Seminar 1 - Basics of
CCS (agents, actions, synchronisation, semaphores):
pdf [186 KB]
- CS238 (Concurrent Processes) Seminar 2 - CCS Examples
(Buffers, Producers/Consumers problem):
pdf
[203 KB]
- CS238 (Concurrent Processes) Seminar 3 - CCS Equivalences
and Bisimulation. Slides (handwritten):
pdf
[260 KB]
- CS406 (Research Directions in Computing) - Revision
class on Quantum Cryptography. Slides (handwritten):
pdf [1,222 KB]
- CS406 (Research Directions in Computing) - Notes on Quantum
Teleportation and Deutsch's algorithm:
pdf
[127 KB]
- CS406 (Research Directions in Computing) - Introduction to Quantum
Cryptography. Lecture, October 2004, Department of Computer Science,
University of Warwick.
pdf [388 KB]
- CS406 (Research Directions in Computing) - Quantum Gates and
Circuits. Lecture, October 2004, Department of Computer Science,
University of Warwick.
pdf
[328 KB]
- CS406 (Research Directions in Computing) - Basics of Quantum
Computation. Lecture, October 2004, Department of Computer Science,
University of Warwick.
pdf
[199 KB]
- CS406 (Research Directions in Computing) - Introduction to Quantum
Cryptography. Lecture, October 2003, Department of Computer Science,
University of Warwick.
pdf
[781 KB]
- University of Warwick Open Day Presentation - Introduction to
Quantum Computation and Quantum Information, October 2003.
pdf
[308 KB]
The content of this webpage is Copyright (c) 2002-2011 of Nikolaos (Nick)
Papanikolaou.
"All points of view are my own and not necessarily HP's as well."
[back to top]
![[European Commission]](EU logo.jpg)
