Document Open Access Logo

Toward Automatic Verification of Quantum Cryptographic Protocols

Authors Yuan Feng, Mingsheng Ying

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.441.pdf
  • Filesize: 0.54 MB
  • 15 pages

Document Identifiers

Author Details

Yuan Feng
Mingsheng Ying

Cite As Get BibTex

Yuan Feng and Mingsheng Ying. Toward Automatic Verification of Quantum Cryptographic Protocols. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 441-455, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CONCUR.2015.441

Abstract

Several quantum process algebras have been proposed and successfully applied in verification of quantum cryptographic protocols. All of the bisimulations proposed so far for quantum processes in these process algebras are state-based, implying that they only compare individual quantum states, but not a combination of them. This paper remedies this problem by introducing a novel notion of distribution-based bisimulation for quantum processes. We further propose an approximate version of this bisimulation that enables us to prove more sophisticated security properties of quantum protocols which cannot be verified using the previous  bisimulations. In particular, we prove that the quantum key distribution protocol BB84 is sound and (asymptotically) secure against the intercept-resend attacks by showing that the BB84 protocol, when executed with such an attacker concurrently, is approximately bisimilar to an ideal protocol, whose soundness and security are obviously guaranteed, with at most an exponentially decreasing gap.

Subject Classification

Keywords
  • Quantum cryptographic protocols
  • Verification
  • Bisimulation
  • Security

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. A. Aldini and A. Di Pierro. Estimating the maximum information leakage. International Journal of Information Security, 7(3):219-242, 2008. Google Scholar
  2. Ebrahim Ardeshir-Larijani, Simon J Gay, and Rajagopal Nagarajan. Equivalence checking of quantum protocols. In TACAS'13, pages 478-492. Springer, 2013. Google Scholar
  3. Ebrahim Ardeshir-Larijani, Simon J Gay, and Rajagopal Nagarajan. Verification of concurrent quantum protocols by equivalence checking. In TACAS'14, pages 500-514. Springer, 2014. Google Scholar
  4. C. H. Bennett and G. Brassard. Quantum cryptography: Public-key distribution and coin tossing. In Proceedings of the IEEE International Conference on Computer, Systems and Signal Processing, pages 175-179, 1984. Google Scholar
  5. T. A. S. Davidson. Formal Verification Techniques using Quantum Process Calculus. PhD thesis, University of Warwick, 2011. Google Scholar
  6. Y. Deng and Y. Feng. Open bisimulation for quantum processes. In TCS'12: Proceedings of the 7th IFIP TC 1/WG 202 international conference on Theoretical Computer Science. Springer-Verlag, September 2012. Full Version available at http://arxiv.org/abs/1201.0416. Google Scholar
  7. Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan. Testing finitary probabilistic processes (extended abstract). In CONCUR'09, pages 274-288. Springer, 2009. Google Scholar
  8. Laurent Doyen, Thomas A Henzinger, and Jean-Francois Raskin. Equivalence of labeled Markov chains. International Journal of Foundations of Computer Science, 19(03):549-563, 2008. Google Scholar
  9. Christian Eisentraut, Jens Chr Godskesen, Holger Hermanns, Lei Song, and Lijun Zhang. Late Weak Bisimulation for Markov Automata. http://arxiv.org/abs/1202.4116, February 2012. Google Scholar
  10. Y. Feng, R. Duan, Z. Ji, and M. Ying. Probabilistic bisimulations for quantum processes. Information and Computation, 205(11):1608-1639, November 2007. Google Scholar
  11. Y. Feng, R. Duan, and M. Ying. Bisimulations for quantum processes. In Mooly Sagiv, editor, POPL'11, pages 523-534, 2011. Google Scholar
  12. Yuan Feng, Yuxin Deng, and Mingsheng Ying. Symbolic bisimulation for quantum processes. ACM Transactions on Computational Logic, 15(2):14:1-14:32, May 2014. Google Scholar
  13. S. J. Gay and R. Nagarajan. Communicating quantum processes. In J. Palsberg and M. Abadi, editors, POPL'05, pages 145-157, 2005. Google Scholar
  14. Holger Hermanns, Jan Krcál, and Jan Kretínský. Probabilistic bisimulation: Naturally on distributions. In Paolo Baldan and Daniele Gorla, editors, CONCUR'14. Springer, 2014. Google Scholar
  15. B. Jonsson, W. Yi, and K. G. Larsen. Probabilistic extensions of process algebras. In Handbook of process algebra, pages 685-710. North-Holland, Amsterdam, 2001. Google Scholar
  16. P. Jorrand and M. Lalire. Toward a quantum process algebra. In P. Selinger, editor, QPL'04, page 111, 2004. Google Scholar
  17. Takahiro Kubota, Yoshihiko Kakutani, Go Kato, Yasuhito Kawano, and Hideki Sakurada. Application of a process calculus to security proofs of quantum protocols. In FCS'12, pages 141-147, 2012. Google Scholar
  18. M Kwiatkowska, G Norman, and D Parker. PRISM 2.0: a tool for probabilistic model checking. In QEST'04, pages 322-323, September 2004. Google Scholar
  19. Marie Lalire. Relations among quantum processes: Bisimilarity and congruence. Mathematical Structures in Computer Science, 16(3):407-428, 2006. Google Scholar
  20. Dominic Mayers. Unconditional security in quantum cryptography. Journal of the ACM, 48(3):351-406, 2001. Google Scholar
  21. J Mitchell, A Ramanathan, A Scedrov, and V Teague. A Probabilistic Polynomial-time Calculus For Analysis of Cryptographic Protocols: (Preliminary Report). Electronic Notes in Theoretical Computer Science, 45:280-310, December 2000. Google Scholar
  22. Rajagopal Nagarajan, Nikolaos Papanikolaou, Garry Bowen, and Simon Gay. An automated analysis of the security of quantum key distribution. In SecCo'05, 2005. Google Scholar
  23. M. Nielsen and I. Chuang. Quantum computation and quantum information. Cambridge university press, 2000. Google Scholar
  24. A. Di Pierro, C. Hankin, and H. Wiklicky. Measuring the confinement of probabilistic systems. Theoretical Computer Science, 340(1):3-56, 2005. Google Scholar
  25. Ajith Ramanathan, John Mitchell, Andre Scedrov, and Vanessa Teague. Probabilistic bisimulation and equivalence for security analysis of network protocols. In FOSSACS'04, pages 468-483. Springer, Berlin, 2004. Google Scholar
  26. Peter W Shor and John Preskill. Simple proof of security of the BB84 quantum key distribution protocol. Physical Review Letters, 85(2):441, 2000. Google Scholar
  27. M. Ying, Y. Feng, R. Duan, and Z. Ji. An algebra of quantum processes. ACM Transactions on Computational Logic, 10(3):1-36, April 2009. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact