Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Journal of Symbolic Computation

Semi-automated verification of security proofs of quantum cryptographic protocols

Takahiro Kubota, Yoshihiko Kakutani, Go Kato, Yasuhito Kawano, Hideki Sakurada

Published Jun 14, 2015• 24 citations
Publisher
DOI
10.1016/j.jsc.2015.05.001

Related papers

Automated Symbolic Verification of Quantum Cryptographic Protocols

Rolando Trujillo-Rasúa, Jesse Laeuchli, Reynaldo Gil-Pons

Lecture notes in computer science•Jan 1, 2026•0 citations

Simplifications of security proofs for cryptographic protocols

一樹 米山

•Jan 1, 2008•0 citations

Automated Verification of Equivalence on Quantum Cryptographic Protocols

Takahiro Kubota, Yoshihiko Kakutani, Go Kato +2 more

t is recognized that security verification of cryptographic protocols tends to be difficult and in fact, some flaws on protocol designs or security proofs were found after they had been presented. The use of formal methods is a way to deal with such complexity. Especially, process calculi are suitable to describe parallel systems. Bisimilarity, which denotes that two processes behave indistinguishably from the outside, is a key notion in process calculi. However, by-hand verification of bisimilarity is often tedious when the processes have many long branches in their transitions. We developed a software tool to automatically verify bisimulation relation in a quantum process calculus qCCS and applied it to Shor and Preskill's security proof of BB84. The tool succeeds to verify the equivalence of BB84 and an EDP-based protocol, which are discussed in their proof.

EPiC series in computing•Jan 23, 2018•1 citation

Security Analysis of Quantum Cryptographic Protocols

Tao Shang, Jianwei Liu

Springer eBooks•Jan 1, 2020•0 citations

Rational cryptography: novel constructions, automated verification and unified definitions

Oana Ciobotaru

Rational cryptography has recently emerged as a very promising field of research by combining notions and techniques from cryptography and game theory, because it offers an alternative to the rather inexible traditional cryptographic model. In contrast to the classical view of cryptography where protocol participants are considered either honest or arbitrarily malicious, rational cryptography models participants as rational players that try to maximize their benefit and thus deviate from the protocol only if they gain an advantage by doing so. The main research goals for rational cryptography are the design of more ecient protocols when players adhere to a rational model, the design and implementation of automated proofs for rational security notions and the study of the intrinsic connections between game theoretic and cryptographic notions. In this thesis, we address all these issues. First we present the mathematical model and the design for a new rational file sharing protocol which we call RatFish. Next, we develop a general method for automated verification for rational cryptographic protocols and we show how to apply our technique in order to automatically derive the rational security property for RatFish. Finally, we study the intrinsic connections between game theory and cryptography by defining a new game theoretic notion, which we call game universal implementation, and by showing its equivalence with the notion of weak stand-alone security.

•Jan 1, 2012•0 citations

GAuV: A Graph-Based Automated Verification Framework for Perfect Semi-Honest Security of Multiparty Computation Protocols

Xingyu Xie, Yifei Li, Wei Zhang +4 more

Proving the security of a Multiparty Computation (MPC) protocol is a difficult task. Under the current simulation-based definition of MPC, a security proof consists of a simulator, which is usually specific to the concrete protocol and requires to be manually constructed, together with a theoretical analysis of the output distribution of the simulator and corrupted parties’ views in the real world. This presents an obstacle in verifying the security of a given MPC protocol. Moreover, an instance of a secure MPC protocol can easily lose its security guarantee due to careless implementation, and such a security issue is hard to detect in practice.(p)(/p)In this work, we propose a general automated framework to verify the perfect security of instances of MPC protocols against the semi-honest adversary. Our framework has perfect soundness: any protocol that is proven secure under our framework is also secure under the simulation-based definition of MPC. We demonstrate the completeness of our framework by showing that for any instance of the well-known BGW protocol, our framework can prove its security for every corrupted party set with polynomial time. Unlike prior work that only focuses on black-box privacy which requires the outputs of corrupted parties to contain no information about the inputs of the honest parties, our framework may potentially be used to prove the security of arbitrary MPC protocols. (p)(/p)We implement our framework as a prototype. The evaluation shows that our prototype automatically proves the perfect semi-honest security of BGW protocols and B2A (binary to arithmetic) conversion protocols in reasonable durations.

IEEE Symposium on Security and Privacy (S&P)•May 19, 2024•3 citations
t is recognized that security verification of cryptographic protocols tends to be difficult and in fact, some flaws on protocol designs or security proofs were found after they had been presented. The use of formal methods is a way to deal with such complexity. Especially, process calculi are suitable to describe parallel systems. Bisimilarity, which denotes that two processes behave indistinguishably from the outside, is a key notion in process calculi. However, by-hand verification of bisimilarity is often tedious when the processes have many long branches in their transitions. We developed a software tool to automatically verify bisimulation relation in a quantum process calculus qCCS and applied it to Shor and Preskill's security proof of BB84. The tool succeeds to verify the equivalence of BB84 and an EDP-based protocol, which are discussed in their proof.
Rational cryptography has recently emerged as a very promising field of research by combining notions and techniques from cryptography and game theory, because it offers an alternative to the rather inexible traditional cryptographic model. In contrast to the classical view of cryptography where protocol participants are considered either honest or arbitrarily malicious, rational cryptography models participants as rational players that try to maximize their benefit and thus deviate from the protocol only if they gain an advantage by doing so. The main research goals for rational cryptography are the design of more ecient protocols when players adhere to a rational model, the design and implementation of automated proofs for rational security notions and the study of the intrinsic connections between game theoretic and cryptographic notions. In this thesis, we address all these issues. First we present the mathematical model and the design for a new rational file sharing protocol which we call RatFish. Next, we develop a general method for automated verification for rational cryptographic protocols and we show how to apply our technique in order to automatically derive the rational security property for RatFish. Finally, we study the intrinsic connections between game theory and cryptography by defining a new game theoretic notion, which we call game universal implementation, and by showing its equivalence with the notion of weak stand-alone security.
Proving the security of a Multiparty Computation (MPC) protocol is a difficult task. Under the current simulation-based definition of MPC, a security proof consists of a simulator, which is usually specific to the concrete protocol and requires to be manually constructed, together with a theoretical analysis of the output distribution of the simulator and corrupted parties’ views in the real world. This presents an obstacle in verifying the security of a given MPC protocol. Moreover, an instance of a secure MPC protocol can easily lose its security guarantee due to careless implementation, and such a security issue is hard to detect in practice.(p)(/p)In this work, we propose a general automated framework to verify the perfect security of instances of MPC protocols against the semi-honest adversary. Our framework has perfect soundness: any protocol that is proven secure under our framework is also secure under the simulation-based definition of MPC. We demonstrate the completeness of our framework by showing that for any instance of the well-known BGW protocol, our framework can prove its security for every corrupted party set with polynomial time. Unlike prior work that only focuses on black-box privacy which requires the outputs of corrupted parties to contain no information about the inputs of the honest parties, our framework may potentially be used to prove the security of arbitrary MPC protocols. (p)(/p)We implement our framework as a prototype. The evaluation shows that our prototype automatically proves the perfect semi-honest security of BGW protocols and B2A (binary to arithmetic) conversion protocols in reasonable durations.