Formal
verification using interactive theorem provers have been noticed as a method of
verification of proofs that are too big for humans to check the validity of
them. The purpose of this work is to verify the validity of Robertson-type
uncertainty relation toward verifying unconditional security of quantum key
distributions. We verify the validity of the relation by using proof assistant
Coq and it is turned out that the theorem regarding the relation formally
holds. The source code for Coq which represents the validity of the theorem is
printed in Appendix.
References
[1]
Gordon, M.J.C. (1986) Why Higher-Order Logic Is a Good Formalism for Specifying and Verifying Hardware. In: Milne, G.J. and Subrahmanyam, P.A., Eds., Proceedings of the 1985 Edinburgh Workshop on VLSI, North-Holland, 153-177.
[2]
Boyer, R.S., Moore, J.S. and Kaufmann, M. (1996) ACL2 Version 7.0. http://www.cs.utexas.edu/users/moore/acl2/
[3]
University of Cambridge Computer Laboratory (1989) Isabelle. http://isabelle.in.tum.de/
[4]
INRIA (1985) The Coq Proof Assistant. http://coq.inria.fr/
[5]
Heine, M., Sørensen, B. and Urzyczyn, P. (2006) Lectures on the Curry-Howard Isomorphism. Warsaw University, Poland.
[6]
Feit, W. and Thompson, J.G. (1963) Solvability of Groups of Odd Order. Pacific Journal of Mathematics, 13, 775-1029. http://dx.doi.org/10.2140/pjm.1963.13.775
[7]
Bender, H. and Glaubernan, G. (1995) Local Analysis for the Odd Order Theorem. Cambridge University Press, Cambridge. http://dx.doi.org/10.1017/CBO9780511665592
[8]
Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O’Connor, R., Biha, S.O., et al. (2013) A Machine-Checked Proof of the Odd Order Theorem. Lecture Notes in Computer Science, 7998, 163-179. http://dx.doi.org/10.1007/978-3-642-39634-2_14
[9]
Affeldt, R., Hagiwara, M. and Sénizergues, J. (2014) Formalization of Shannon’s Theorems. Journal of Automated Reasoning, 53, 63-103. http://dx.doi.org/10.1007/s10817-013-9298-1
[10]
Shannon, C.E. (1948) A mathematical Theory of Communication. Bell System Technical Journal, 27, 379-423. http://dx.doi.org/10.1002/j.1538-7305.1948.tb01338.x
[11]
Hayashi, M., Ishizaka, S., Kawachi, A., Kimura, G. and Ogawa, T. (2014) Introduction to Quantum Information Science. Springer.
Bennett, C.H. and Brassard, G. (1984) Quantum Cryptography: Public Key Distribution and Coin Tossing. Proceedings of IEEE International Conference on Computers Systems and Signal Processing, Bangalore, 175-179.
[14]
Biham, E., Boyer, M., Boykin, P.O., Mor, T. and Roychowdhury, V. (2000) A Proof of the Security of Quantum Key Distribution. Proceedings of 32nd Annual ACM Symposium on the Theory of Computing, New York, 715-724.
[15]
Miyadera, T. and Imai, H. (2006) Information-Disturbance Theorem for Mutually Unbiased Observables. Physical Review A, 73, Article ID: 042317. http://dx.doi.org/10.1103/PhysRevA.73.042317
[16]
Miyadera, T. and Imai, H. (2007) Information-Disturbance Theorem and Uncertainty Relation. http://arxiv.org/abs/0707.4559
[17]
Maassen, H. and Uffink, J.B.M. (1988) Generalized Entropic Uncertainty Relations. Physical Review Letters, 60, 1103. http://dx.doi.org/10.1103/PhysRevLett.60.1103
[18]
Krishna, M. and Parthasarathy, K.R. (2002) An Entropic Uncertainty Principle for Quantum Measurements. Sankhya: The Indian Journal of Statistics, Series A, 64, 842-852.
