Research ArticleOpen AccessGoogle Scholar indexed
Formal Verification of Robertson-Type Uncertainty Relation
Department of Intelligent Information Engineering and Sciences, Doshisha University, Kyoto, Japan
Department of Intelligent Information Engineering and Sciences, Doshisha University, Kyoto, Japan
Department of Intelligent Information Engineering and Sciences, Doshisha University, Kyoto, Japan
Department of Intelligent Information Engineering and Sciences, Doshisha University, Kyoto, Japan
- 1 Department of Intelligent Information Engineering and Sciences, Doshisha University, Kyoto, Japan
- 2 Department of Intelligent Information Engineering and Sciences, Doshisha University, Kyoto, Japan
- 3 Department of Intelligent Information Engineering and Sciences, Doshisha University, Kyoto, Japan
- 4 Department of Intelligent Information Engineering and Sciences, Doshisha University, Kyoto, Japan
Journal of Quantum Information Science·Volume 05 (2015)·Pages 58–70·Published 28 May 2015·DOI10.4236/jqis.2015.52008
Copy link · social · email
Abstract
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 .
KeywordsFormal VerificationProof Assistant CoqUncertainty Relation
- 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.
- Boyer, R.S., Moore, J.S. and Kaufmann, M. (1996) ACL2 Version 7.0. http://www.cs.utexas.edu/users/moore/acl2/
- University of Cambridge Computer Laboratory (1989) Isabelle. http://isabelle.in.tum.de/
- INRIA (1985) The Coq Proof Assistant. http://coq.inria.fr/
- Heine, M., Sørensen, B. and Urzyczyn, P. (2006) Lectures on the Curry-Howard Isomorphism. Warsaw University, Poland.
- 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
- Bender, H. and Glaubernan, G. (1995) Local Analysis for the Odd Order Theorem. Cambridge University Press, Cambridge. http://dx.doi.org/10.1017/CBO9780511665592
- 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
- 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
- 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
- Hayashi, M., Ishizaka, S., Kawachi, A., Kimura, G. and Ogawa, T. (2014) Introduction to Quantum Information Science. Springer.
- Robertson, H.P. (1929) The Uncertanty Principle. Physical Review, 34, 163-164. http://dx.doi.org/10.1103/PhysRev.34.163
- 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.
- 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.
- 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