Basic protocols in quantum communication

Yu Yang

The quantum communication is one of the most important technologies, which is the combination of quantum mechanics and cryptography.Introduced the principle and method of quantum communication and three protocol distribute. Instruct some problem of to develop quantum communication.

Masahito Hayashi

Sheng Zhang, Yonghui Ma, Chunning Meng +1 more

This paper presents a new formal method for verification of quantum communication protocols. By extending the symbolic system of Petri nets, we can define quantum pure states in Petri-net settings. Therefore, it is possible to emerge a framework from formalizing basic quantum phenomena, which are utilized to achieve communication tasks. We also present an example of applying this framework to the modeling and analyzing quantum communication protocols to show how it works.

Chitra Shukla

Canh Minh Do, Tsubasa Takagi, Kazuhiro Ogata

While constructing practical quantum computers by big companies remains a challenge, the application of quantum communication and cryptography has made remarkable progress. Therefore, it is crucial to verify quantum protocols before they can be trusted in safety and security-critical applications. We have proposed Basic Dynamic Quantum Logic (BDQL) to formalize and verify sequential models of quantum protocols with a support tool developed in Maude. However, BDQL does not support concurrency in its formalization. This article introduces Concurrent Dynamic Quantum Logic (CDQL), an extension of BDQL, to formalize and verify concurrent models of quantum protocols. CDQL is more expressive than BDQL by considering concurrent behavior and communication among participants in quantum protocols. Since CDQL is a conservative extension of BDQL, we extend the syntax of BDQL to CDQL and make a transformation from CDQL to BDQL without interrupting the semantics of BDQL. We also extend the implementation of BDQL to support CDQL, making a new support tool in Maude. The new support tool is equipped with a lazy rewriting strategy to make the verification process significantly faster. Several quantum communication protocols are successfully formalized and verified in BDQL/CDQL, demonstrating the effectiveness of our automated approach and tool in verifying quantum protocols.