Verification of quantum cryptographic protocols: a process algebra approach

Funding: 2016: $120,000
2017: $120,000
2018: $120,000

Project Member(s): Ying, M., Feng, Y.

Funding or Partner Organisation: Australian Research Council (ARC Discovery Projects)

Start year: 2016

Summary: Security analysis of quantum cryptographic systems is notoriously difficult. This project aims to develop theoretic foundations and algorithms, as well as efficient software tools, for the verification of quantum cryptographic protocols by innovatively bridging two research fields: quantum cryptography and quantum process algebra. The pioneering research will improve Australia’s standing in scientific research internationally and provide innovative, game-changing security technologies for banks, business, finance, security industry, police, and counter-terrorism both within Australia and globally.

Publications:

Barthe, G, Hsu, J, Ying, M, Yu, N & Zhou, L 2020, 'Relational proofs for quantum programs.', Proc. ACM Program. Lang., vol. 4, no. POPL, pp. 21:1-21:1.
View/Download from: Publisher's site

Guan, J, Feng, Y, Turrini, A & Ying, M 2019, 'Model Checking Applied to Quantum Physics.', CoRR, vol. abs/1902.03218.

Li, G, Zhou, L, Yu, N, Ding, Y, Ying, M & Xie, Y 2019, 'Poq: Projection-based Runtime Assertions for Debugging on a Quantum Computer.', CoRR, vol. abs/1911.12855.

Liu, J, Zhou, L & Ying, M 2019, 'Expected Runtime of Quantum Programs.', CoRR, vol. abs/1911.12557.

Wang, Q, Liu, J & Ying, M 2019, 'Equivalence Checking of Quantum Finite-State Machines.', CoRR, vol. abs/1901.02173, pp. 1-21.
View/Download from: Publisher's site

Ying, M 2019, 'Toward automatic verification of quantum programs.', Formal Aspects Comput., vol. 31, pp. 3-25.
View/Download from: Publisher's site

Liu, J, Zhan, B, Wang, S, Ying, S, Liu, T, Li, Y, Ying, M & Zhan, N 1970, 'Quantum Hoare Logic.', Arch. Formal Proofs.

Barthe, G, Hsu, J, Ying, M, Yu, N & Zhou, L 2019, 'Coupling Techniques for Reasoning about Quantum Programs.'.

Guan, J, Feng, Y & Ying, M 2018, 'Super-activating quantum memory with entanglement.', Quantum Inf. Comput., vol. 18, no. 13&14, pp. 1115-1124.
View/Download from: Publisher's site

Li, Y & Ying, M 2018, 'Algorithmic analysis of termination problems for quantum programs.', Proc. ACM Program. Lang., vol. 2, pp. 35:1-35:1.
View/Download from: Publisher's site

Su, Z, Li, L & Ling, J 2018, 'An approach for quantitatively analyzing the genuine tripartite nonlocality of general three-qubit states', Quantum Information Processing, vol. 17, no. 4.
View/Download from: Publisher's site

Ying, M 2018, 'Toward Automatic Verification of Quantum Programs.', CoRR, vol. abs/1807.11610, no. 1, pp. 3-25.
View/Download from: Publisher's site

Ying, M & Feng, Y 2018, 'Model Checking Quantum Systems - A Survey.', CoRR, vol. abs/1807.09466, no. 1, pp. 28-31.
View/Download from: Publisher's site

Zhou, L, Ying, S, Yu, N & Ying, M 2018, 'Quantum Coupling and Strassen Theorem.', CoRR, vol. abs/1803.10393.

Fu, C, Turrini, A, Huang, X, Song, L, Feng, Y & Zhang, L 1970, 'Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems', Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, Twenty-Seventh International Joint Conference on Artificial Intelligence {IJCAI-18}, International Joint Conferences on Artificial Intelligence Organization, Stockholm, Sweden, pp. 4757-4763.
View/Download from: Publisher's site

Hung, S-H, Hietala, K, Zhu, S, Ying, M, Hicks, M & Wu, X 2018, 'Quantitative Robustness Analysis of Quantum Programs (Extended Version).', CoRR.

Wang, Q & Ying, M 2018, 'Quantum Büchi Automata.', CoRR.

Ying, M & Li, Y 2018, 'Reasoning about Parallel Quantum Programs.'.

Ying, S & Ying, M 2018, 'Reachability analysis of quantum Markov decision processes.', pp. 31-51.
View/Download from: Publisher's site

Deng, Y & Feng, Y 2017, 'Probabilistic bisimilarity as testing equivalence', Information and Computation, vol. 257, pp. 58-64.
View/Download from: Publisher's site

Feng, Y & Zhang, L 2017, 'Precisely deciding CSL formulas through approximate model checking for CTMCs', Journal of Computer and System Sciences, vol. 89, pp. 361-371.
View/Download from: Publisher's site

Su, Z 2017, 'Generating tripartite nonlocality from bipartite resources', Quantum Information Processing, vol. 16, no. 1, pp. 1-13.
View/Download from: Publisher's site

Su, Z, Guan, J & Li, L 2017, 'Efficient quantum repeater in perspectives of both entanglement concentration rate and LOCC complexity', Phys. Rev. A, vol. 97, no. 1, p. 012325.
View/Download from: Publisher's site

Deng, Y & Feng, Y 1970, 'Bisimulations for probabilistic linear lambda calculi', 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE), 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE), IEEE, Sophia Antipolis, France, pp. 1-8.
View/Download from: Publisher's site

Su, G, Chen, T, Feng, Y & Rosenblum, DS 1970, 'ProEva: Runtime Proactive Performance Evaluation Based on Continuous-Time Markov Chains', 2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE), 2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE), IEEE, Buenos Aires, Argentina, pp. 484-495.
View/Download from: Publisher's site

Ying, S, Ying, M & Feng, Y 2017, 'Quantum Privacy-Preserving Data Analytics.'.

Ying, S, Ying, M & Feng, Y 2017, 'Quantum Privacy-Preserving Perceptron.'.

Ying, M 2016, Foundations of Quantum Programming, Morgan Kaufmann Publishers.
View/Download from: Publisher's site

Su, G, Chen, T, Feng, Y, Rosenblum, DS & Thiagarajan, PS 1970, 'An Iterative Decision-Making Scheme for Markov Decision Processes and Its Application to Self-adaptive Systems', Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Fundamental Approaches to Software Engineering, Springer Berlin Heidelberg, Eindhoven, The Netherlands, pp. 269-286.
View/Download from: Publisher's site

Liu, T, Li, Y, Wang, S, Ying, M & Zhan, N 2016, 'A Theorem Prover for Quantum Hoare Logic and Its Applications'.

Feng, Y & Ying, M 1970, 'Toward automatic verification of quantum cryptographic protocols', Leibniz International Proceedings in Informatics, LIPIcs, International Conference on Concurrency Theory, Springer, Spain, pp. 441-455.
View/Download from: Publisher's site

Feng, Y & Ying, M 1970, 'Toward Automatic Verification of Quantum Cryptographic Protocols.', CONCUR, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 441-455.

Ying, M 2014, 'Quantum Recursion and Second Quantisation'.

Ying, M, Li, Y, Yu, N & Feng, Y 2011, 'Model-Checking Linear-Time Properties of Quantum Systems'.

Ying, M 1970, 'Foundations of Quantum Programming (Extended Abstract)', PROGRAMMING LANGUAGES AND SYSTEMS, Programming Languages and Systems, Springer-Verlag, Shanghai, China, pp. 16-20.
View/Download from: Publisher's site

Keywords: Quantum cryptography; Quantum process algebra; Security analysis; Bisimulation

FOR Codes: Computational Logic and Formal Languages, Expanding Knowledge in the Information and Computing Sciences, Information and Communication Services not elsewhere classified, Other information and communication services not elsewhere classified

Acknowledgement of Country

UTS acknowledges the Gadigal people of the Eora Nation, the Boorooberongal people of the Dharug Nation, the Bidiagal people and the Gamaygal people, upon whose ancestral lands our university stands. We would also like to pay respect to the Elders both past and present, acknowledging them as the traditional custodians of knowledge for these lands.