|
|
- 2017
基于模型检测的半量子密码协议的安全性分析
|
Abstract:
对于密码协议而言，安全性是其最核心的关键问题，对于量子密码协议来说也一样。研究人员可以通过各种手段证明这些协议是安全的，但存在极大的困难，因为这对数学功底有着很高的要求。该文利用全自动化的技术——模型检测，采用了形式化验证方法，即基于概率的模型检测工具PRISM，来对半量子密码协议进行建模并验证其安全性。该方法避免了传统基于数学方法验证的繁杂，提高了验证的速度和效率。验证的结果也表明，当传输足够多的光子时，检测出窃听的概率无限趋近于1，和全量子密码协议一样，半量子密码协议也是安全的。
| [1] | BENNETT C H, BRASSARD G. Quantum cryptography:Public key distribution and coin tossing[C]//In Proc of IEEE International Conference on Computers, Systems, and Signal Processing. Bangalore, India:IEEE, 1984:175-179. |
| [2] | BASAGIANNIS S, KATSAROS P, POMBORTSIS A. Synthesis of attack actions using model checking for the verification of security protocols[J]. Secur Comm Networks, 2011, 4(2):147-161. |
| [3] | ELBOUKHARI M, AZIZI M. Analysis of the security of bb84 by model checking[J]. International Journal of Network Security & Its Applications, 2010, 2(2):87-98. |
| [4] | CHANG Y J, TSAI C W, HWANG T. Multi-user private comparison protocol using GHz class states[J]. Quantum Information Processing, 2013, 12(2):1077-1088. |
| [5] | YANG F, YANG G W, HAO Y J, et al. Security analysis of multi-party quantum private comparison protocol by model checking[J]. Modern Physics Letters B, 2015, 29(18):717-755. |
| [6] | YANG F, YANG G W, HAO Y J. The modeling library of eavesdropping methods in quantum cryptography protocols by model checking[J]. International Journal of Theoretical Physics, 2016, DOI:10.1007/s10773-016-2969-z. |
| [7] | HILLERY M, BUZEK V, BERTHIAUME A. Quantum secret sharing[J]. Physical Review A, 1999, 59(3):1829-1834. |
| [8] | CHUANG I, GOTTESMAN D. Quantum digital signatures:US, US 7246240 B2[P]. 2007. |
| [9] | ZENG G H, CHRISTOPH K. An arbitrated quantum signature scheme[J]. Physev A, 2002, 65:042312. |
| [10] | BOYER M, KENIGSBERG D, MOR T. Quantum key distribution with classical bob[C]//First International Conference on Quantum, Nano, and Micro Technologies, 2007, ICQNM'07.[S.l.]:IEEE, 2007, 99(14):10-10. |
| [11] | KRAWEC W. Mediated semiquantum key distribution[J]. Physical Review A, 2015, 91(3):032323. |
| [12] | BOYER M, GELLES R, KENIGSBERG D, et al. Semiquantum key distribution[J]. Phys Rev A, 2009, 79:032341. |
| [13] | YU K F, YANG C W, LIAO C H, et al. Authenticated semi-quantum key distribution protocol using Bell states[J]. Quantum Information Processing, 2014, 13(6):1-9. |
| [14] | KRAWEC W. Mediated semiquantum key distribution[J]. Physical Review A, 2015, 91(3):032323. |
| [15] | KRAWEC W. Security proof of a semi-quantum key distribution protocol to appear[C]//IEEE ISIT 2015.[S.l.]:IEEE, 2015. |
| [16] | KRAWEC W. Semi-quantum key distribution[D].[S.l.]:Stevens Institute of Technology, 2015. |
| [17] | QUEILLE J P, SIFAKIS J. Specification and verification of concurrent systems in CESAR[C]//In Proc 5th Colloquium on Int Symp Programming. London:Springer, 1982:337-351. |
| [18] | BEN-ARI M, PNUELI A, MANNA Z. The temporal logic of branching time[J]. Acta Informatica, 1983, 20(3):207-226. |
| [19] | GASTIN P, ODDOUX D. Fast LTL to büchi automata translation[J]. Lecture Notes in Computerence, 2001, 2102:53-65. |
| [20] | YANG J, SEGER C H J. Generalized symbolic trajectory evaluation-abstraction in action[M]//Formal Methods in Computer-Aided Design, LNCS. Berlin, Heidelberg:Springer-Verlag, 2002:70-87. |
| [21] | BENNETT C H, BESSETTE F, BRASSARD G, et al. Experimental quantum cryptography[J]. Journal of Cryptology, 1992, 5(1):3-28. |
| [22] | SHI R H, HUANG L S, YANG W, et al. Multiparty quantum secret sharing with Bell states and Bell measurements[J]. Optics Communications, 2010, 283(11):2476-2480. |
| [23] | RAHAMAN R, PARKER M G. Quantum scheme for secret sharing based on local distinguishability[J]. Physical Review A, 2015, 91(2):91. 022330. |
| [24] | KRAWEC W. Security of a semi-quantum protocol where reflections contribute to the secret key[J]. Quantum Information Processing, 2015, 15(5):1-24. |
| [25] | KRAWEC W. Restricted attacks on semi-quantum key distribution protocols[J]. Quantum Information Processing, 2014, 13(11):2417-2436. |
| [26] | BAIER C, KATOEN J P. Principles of model checking[M]. Cambridge, USA:The MIT Press, 2008. |
| [27] | EMERSON E A, CLARKE E M. Characterizing correctness properties of parallel programs using fixpoints[M]//Automata, Languages and Programming. Berlin, Heidelberg:Springer-Verlag, 1980:169-181. |
| [28] | CLARKE E M, EMERSON E A. Design and synthesis of synchronization skeletons using branching time temporal logic[J]. Proc Workshop on Logic of Programs, 1982, 131:52-71. |
| [29] | CLARKE E M, EMERSON E A, SISTLA A P. Automatic verification of finite-state concurrent systems using temporal logic specifications[C]//ACM Transactions on Programming Languages and Systems. New York:ACM, 1986:244-263. |
