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 paper 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.
@article{CanhTosem24,author={Do, Canh Minh and Takagi, Tsubasa and Ogata, Kazuhiro},title={Automated Quantum Protocol Verification Based on Concurrent Dynamic Quantum Logic},year={2024},publisher={Association for Computing Machinery},address={New York, NY, USA},issn={1049-331X},note={Just Accepted},journal={ACM Transactions on Software Engineering and Methodology},month=dec,keywords={Concurrent Dynamic Quantum Logic, Parallel Composition, Quantum Protocols, Maude}}
2023
DaLí
Automated Quantum Program Verification in Dynamic Quantum Logic
@inproceedings{TsubasaDali23,author={Takagi, Tsubasa and Do, Canh Minh and Ogata, Kazuhiro},editor={Gierasimczuk, Nina and Vel{\'a}zquez-Quesada, Fernando R.},title={Automated Quantum Program Verification in Dynamic Quantum Logic},booktitle={Dynamic Logic. New Trends and Applications},year={2023},publisher={Springer Nature Switzerland},address={Cham},pages={68--84},isbn={978-3-031-51777-8}}
FAVPQC
Automated Quantum Program Verification in Probabilistic Dynamic Quantum Logic
@inproceedings{Canh23PDQL,author={Minh Do, Canh and Takagi, Tsubasa and Ogata, Kazuhiro},title={Automated Quantum Program Verification in Probabilistic Dynamic Quantum Logic},booktitle={The 2nd International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols (collocated at ICFEM 2023)},year={2023}}