A Formal Approach to Unconditional Security Proofs for Quantum Key Distribution. - Takahiro Kubota; Yoshihiko Kakutani; Go Kato; Yasuhito Kawano (UC, 2011)

Automated Verification of Equivalence on Quantum Cryptographic Protocols. - Takahiro Kubota; Yoshihiko Kakutani; Go Kato; Yasuhito Kawano; Hideki Sakurada (SCSS, 2013)

Observational Equivalence Using Schedulers for Quantum Processes. - Kazuya Yasuda; Takahiro Kubota; Yoshihiko Kakutani (QPL, 2014)

Semi-automated verification of security proofs of quantum cryptographic protocols. - Takahiro Kubota; Yoshihiko Kakutani; Go Kato; Yasuhito Kawano; Hideki Sakurada (J. Symb. Comput., 2016)