An Automated Analysis of the Security of Quantum Key Distribution

by Rajagopal Nagarajan, Nikolaos Papanikolaou, Garry Bowen, Simon Gay
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.
Reference:
An Automated Analysis of the Security of Quantum Key Distribution (Rajagopal Nagarajan, Nikolaos Papanikolaou, Garry Bowen, Simon Gay), In Proceedings of the Third International Workshop on Security Issues in Concurrency (SECCO’05), 2005.
Bibtex Entry:
@INPROCEEDINGS{Nagarajan2005,
  author = {Rajagopal Nagarajan and Nikolaos Papanikolaou and Garry Bowen and
	Simon Gay},
  title = {An Automated Analysis of the Security of Quantum Key Distribution},
  booktitle = {Proceedings of the Third International Workshop on Security Issues
	in Concurrency (SECCO'05)},
  year = {2005},
  address = {San Francisco, USA},
  month = aug,
  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.},
  owner = {Nick},
  timestamp = {2010.06.20},
  url = {../files/NRG-secco05.pdf}
}