Semi-automated verification of security proofs of quantum cryptographic protocols

DOI10.1016/J.JSC.2015.05.001MaRDI QIDQ491263zbMATH OpenOpenAlexWikidataFDO

Authors Takahiro Kubota, Yoshihiko Kakutani, Go Kato, Y. Kawano, Hideki Sakurada

Publication date 24 August 2015

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jsc.2015.05.001

zbMATH Keywords

formal methodsquantum key distributionprocess calculiquantum protocolssemi-automated verification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Quantum cryptography (quantum-theoretic aspects) (81P94)

Recommendations

• Toward automatic verification of quantum cryptographic protocols
• Security analysis of semi-quantum cryptography protocols by model checking
• Specification and verification of quantum protocols
• A formal approach to unconditional security proofs for quantum key distribution
• Model checking quantum Markov chains

Cites work

• scientific article; zbMATH DE number 1296290 (Why is no real title available?)
• scientific article; zbMATH DE number 1842495 (Why is no real title available?)
• A process algebra for reasoning about quantum security
• An algebra of quantum processes
• Analysis of a quantum error correcting code using quantum process calculus
• Automata, Languages and Programming
• Bisimulation for quantum processes
• Equivalence checking of quantum protocols
• New directions in cryptography
• Open bisimulation for quantum processes
• Probabilistic bisimulations for quantum processes
• Proof of unconditional security of six-state quantum key distribution scheme
• Quantum computation and quantum information. 10th anniversary edition
• Quantum cryptography using any two nonorthogonal states
• Relations among quantum processes: bisimilarity and congruence
• Towards a quantum programming language
• Unconditional security in quantum cryptography

Cited in

(9)

• Toward automatic verification of quantum cryptographic protocols
• Verifying quantum communication protocols with ground bisimulation
• On well-founded and recursive coalgebras
• Automated verification of quantum protocols using \textsc{mcmas}
• verifier
• Symbolic bisimulation for quantum processes
• Security analysis of semi-quantum cryptography protocols by model checking
• Bisimulations for probabilistic and quantum processes (invited paper)
• Toward automatic verification of quantum programs

Describes a project that uses

Uses Software

• QPL
• PRISM

This page was built for publication: Semi-automated verification of security proofs of quantum cryptographic protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q491263)