Abstract
The novel field of quantum computation and quantum information has been growing at a rapid rate; the study of quantum information in particular has led to the emergence of communication and cryptographic protocols with no classical analogues. Quantum information protocols have interesting properties which are not exhibited by their classical counterparts, but they are most distinguished for their applications in cryptography. Notable results include the unconditional security proof [1] of quantum key distribution. This result, in particular, is one of the reasons for the widespread interest in this field. Furthermore, the implementation of quantum cryptography has been demonstrated in non-laboratory settings and is already an important practical technology. Implementations of quantum cryptography have already been commercially launched and tested by a number of companies including MagiQ, Id Quantique, Toshiba, and NEC. The unconditional security of quantum key distribution protocols does not automatically imply the same degree of security for actual systems, of course; this justifies the need for systems modelling and verification in this setting.
Chapter PDF
Similar content being viewed by others
References
Mayers, D.: Unconditional security in quantum cryptography. Journal of the ACM 48(3), 351–406 (2001)
Gay, S.J., Nagarajan, R., Papanikolaou, N.: Probabilistic model–checking of quantum protocols. In: DCM 2006: Proceedings of the 2nd International Workshop on Developments in Computational Models (2006) arXiv:quant-ph/0504007
Baltazar, P., Chadha, R., Mateus, P., Sernadas, A.: Towards model-checking quantum security protocols. In: Dini, P., et al. (eds.) Proceedings of the First Workshop on Quantum Security: QSec 2007, IEEE Press, Los Alamitos (2007)
Gottesman, D.: The Heisenberg representation of quantum computers. In: Corney, S., Delbourgo, R., Jarvis, P. (eds.) Group22: Proceedings of the XXII International Colloquium on Group Theoretical Methods in Physics. International Press (1999)
Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press, Cambridge (2000)
Bennett, C.H., Brassard, G.: Quantum Cryptography: Public key distribution and coin tossing. In: Proceedings of International Conference on Computers, Systems and Signal Processing (1984)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach. In: POPL 1983: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 117–126. ACM, New York (1983)
Aaronson, S., Gottesman, D.: Improved simulation of stabilizer circuits. Physical Review A 70(52328) (2004)
Audenaert, K., Plenio, M.: Entanglement on mixed stabiliser states: Normal forms and reduction procedures. New Journal of Physics 7(170) (2005)
Bravyi, S., Kitaev, A.: Universal quantum computation with ideal Clifford gates and noisy ancillas. Physical Review A 71, 1–14 (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gay, S.J., Nagarajan, R., Papanikolaou, N. (2008). QMC: A Model Checker for Quantum Systems. In: Gupta, A., Malik, S. (eds) Computer Aided Verification. CAV 2008. Lecture Notes in Computer Science, vol 5123. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70545-1_51
Download citation
DOI: https://doi.org/10.1007/978-3-540-70545-1_51
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70543-7
Online ISBN: 978-3-540-70545-1
eBook Packages: Computer ScienceComputer Science (R0)