@inproceedings{c8de6df1918343409b8e1b01e1cfe1a2,
title = "Model checking quantum key distribution protocols",
abstract = "Quantum key distribution protocols use quantum information theories to guarantee the security of key exchange procedure, and model checking is a verification technique which could be used to test the security of it. In this paper, a new group quantum key distribution protocol is designed based on BB84 protocol, which is a possible solution to handle the security issue in communication between multi-users. Discrete time Markov chain and probabilistic computation tree logic are used to model the protocol procedure and verify its security properties in PRISM. Also, we provide the theoretical proof for this group protocol, which supports the model checking results from PRISM. Our study gives an insight into some of the major difficulties of quantum security protocol design and analysis.",
keywords = "BB84, Group QKD, Model checking",
author = "Baichuan Huang and Yan Huang and Jiaming Kong and Xin Huang",
note = "Publisher Copyright: {\textcopyright} 2016 IEEE.; 8th International Conference on Information Technology in Medicine and Education, ITME 2016 ; Conference date: 23-12-2016 Through 25-12-2016",
year = "2017",
month = jul,
day = "12",
doi = "10.1109/ITME.2016.0144",
language = "English",
series = "Proceedings - 2016 8th International Conference on Information Technology in Medicine and Education, ITME 2016",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "611--615",
editor = "Ying Dai and Shaozi Li and Yun Cheng",
booktitle = "Proceedings - 2016 8th International Conference on Information Technology in Medicine and Education, ITME 2016",
}