A Role-Based Specification of the SET Payment Transaction Protocol. - Hideki Sakurada; Yasuyuki Tsukada (Network Security, 2001)

A Formal Approach to Designing Anonymous Software. - Yoshinobu Kawabe; Hideki Sakurada (SERA, 2007)

Theorem-proving anonymity of infinite-state systems. - Yoshinobu Kawabe; Ken Mano; Hideki Sakurada; Yasuyuki Tsukada (Inf. Process. Lett., 2007)

On Backward-Style Anonymity Verification. - Yoshinobu Kawabe; Ken Mano; Hideki Sakurada; Yasuyuki Tsukada (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2008)

An Adversary Model for Simulation-Based Anonymity Proof. - Yoshinobu Kawabe; Hideki Sakurada (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2008)

Computationally Sound Formalization of Rerandomizable RCCA Secure Encryption. - Yusuke Kawamoto 001; Hideki Sakurada; Masami Hagiya (Formal to Practical Security, 2009)

Computational and Symbolic Anonymity in an Unbounded Network. - Hubert Comon-Lundh; Yusuke Kawamoto 001; Hideki Sakurada (JSIAM Lett., 2009)

Role Interchange for Anonymity and Privacy of Voting. - Ken Mano; Yoshinobu Kawabe; Hideki Sakurada; Yasuyuki Tsukada (J. Log. Comput., 2010)

Probabilistic anonymity via coalgebraic simulations. - Ichiro Hasuo; Yoshinobu Kawabe; Hideki Sakurada (Theor. Comput. Sci., 2010)

Anonymity, Privacy, Onymity, and Identity: A Modal Logic Approach. - Yasuyuki Tsukada; Ken Mano; Hideki Sakurada; Yoshinobu Kawabe (Trans. Data Priv., 2010)

Automatic verification of anonymity of protocols. - Hideki Sakurada (JSIAM Lett., 2011)

Computationally Complete Symbolic Attacker in Action. - Gergei Bana; Pedro Adão; Hideki Sakurada (FSTTCS, 2012)

Computational Soundness of Indistinguishability Properties without Computable Parsing. - Hubert Comon-Lundh; Masami Hagiya; Yusuke Kawamoto 001; Hideki Sakurada (ISPEC, 2012)

Computationally Sound Verification of the NSL Protocol via Computationally Complete Symbolic Attacker. - Gergei Bana; Pedro Adão; Hideki Sakurada (IACR Cryptol. ePrint Arch., 2012)

Computational Soundness of Symbolic Blind Signatures under Active Attacker. - Hideki Sakurada (FPS, 2013)

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

An Epistemic Approach to Compositional Reasoning about Anonymity and Privacy. - Yasuyuki Tsukada; Hideki Sakurada; Ken Mano; Yoshifumi Manabe (TARK, 2013)

Analyzing and Fixing the QACCE Security of QUIC. - Hideki Sakurada; Kazuki Yoneyama; Yoshikazu Hanatani; Maki Yoshida (SSR, 2016)

On compositional reasoning about anonymity and privacy in epistemic logic. - Yasuyuki Tsukada; Hideki Sakurada; Ken Mano; Yoshifumi Manabe (Ann. Math. Artif. Intell., 2016)

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

Trust Trust Me (The Additivity). - Ken Mano; Hideki Sakurada; Yasuyuki Tsukada (IFIPTM, 2017)

Research Directions in Formal Verification of Network Configurations Toward Verification of Mobile Networks. - Hideki Sakurada; Kouichi Sakurai (MobiSec, 2023)

Quality and Quantity Pair as Trust Metric. - Ken Mano; Hideki Sakurada; Yasuyuki Tsukada (IEICE Trans. Inf. Syst., 2023)

SoK: Directions and Issues in Formal Verification of Payment Protocols. - Hideki Sakurada; Kouichi Sakurai (AINA (4), 2024)