2026
Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek:
Symbolic Analysis and Verification of Hybrid Post-Quantum TLS 1.2. IEEE Access 14: 66993-67008 (2026)
2025
Víctor García, Santiago Escobar, Kazuhiro Ogata:
Formalization and analysis of the post-quantum signature scheme FALCON with Maude. J. Log. Algebraic Methods Program. 143: 101034 (2025)
Canh Minh Do, Adrián Riesco, Santiago Escobar, Kazuhiro Ogata:
Parallel Maude-NPA for Cryptographic Protocol Analysis. IEEE Trans. Dependable Secur. Comput. 22(6): 6714-6731 (2025)
2024
Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani:
Formal Analysis of Post-Quantum Hybrid Key Exchange SSH Transport Layer Protocol. IEEE Access 12: 1672-1687 (2024)
2023
Ayoub Otmani, Christophe Petit, Mehdi Tibouchi:
Guest Editorial: Guest Editorial on Cryptanalysis of (NIST PQC) post-quantum proposals. IET Inf. Secur. 17(2): 159-160 (2023)
Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani:
Kyber, Saber, and SK- MLWR lattice-based key encapsulation mechanisms model checking with Maude. IET Information Security, 2023
Víctor García, Santiago Escobar, Kazuhiro Ogata, Sedat Akleylek, Ayoub Otmani:
Modelling and verification of post-quantum key encapsulation mechanisms using Maude. PeerJ Comput. Sci. 9 2023
Duong Dinh Tran, Canh Minh Do, Santiago Escobar, Kazuhiro Ogata:
Hybrid post-quantum Transport Layer Security formal analysis in Maude-NPA and its parallel version. PeerJ Comput. Sci. 9 2023
Duong Dinh Tran, Thet Wai Mon, Kazuhiro Ogata:
Transport
Layer Security 1.0 handshake protocol formal verification case study:
How to use a proof script generator for existing large proof scores. PeerJ Comput. Sci. 9 2023
Meryem Soysaldi Sahin, Sedat Akleylek:
A survey of quantum secure group signature schemes: Lattice-based approach.J. Inf. Secur. Appl. 73
Fan Yang, Santiago Escobar, Catherine A. Meadows, José Meseguer, Sonia Santiago:
Strand Spaces with Choice via a Process Algebra Semantics. Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems 2023
2022
Duong Dinh Tran, Kazuhiro Ogata:
Formal verification of TLS 1.2 by automatically generating proof scores.Comput. Secur. 2022
Duong Dinh Tran, Kazuhiro Ogata:
IPSG: Invariant Proof Score Generator. COMPSAC 2022
Kübra Seyhan, Tu N. Nguyen, Sedat Akleylek, Korhan Cengiz:
Lattice-based cryptosystems for the security of resource-constrained IoT devices in post-quantum world: a survey.Clust. Comput. 25(3)
Kübra Seyhan, Sedat Akleylek:
Classification of random number generator applications in IoT: A comprehensive taxonomy.J. Inf. Secur. Appl. 71
Meryem Soysaldi, Sedat Akleylek:
A constant-size lattice-based partially-dynamic group signature scheme in quantum random oracle model. J. King Saud Univ. Comput. Inf. Sci. 34(10 Part B)
Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani:
Formal specification and model checking of Saber lattice-based key encapsulation mechanism in Maude. SEKE 2022
Francisco Durán, Steven Eker, Santiago Escobar, Narciso Martí-Oliet, José Meseguer, Rubén Rubio, Carolyn L. Talcott:
Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description).IJCAR 2022
Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, Ayoub Otmani:
Formal specification and model checking of lattice-based key encapsulation mechanisms in Maude. FAVPQC@ICFEM 2022
Raúl López-Rueda, Santiago Escobar:
Canonical Narrowing for Variant-Based Conditional Rewrite Theories. ICFEM 2022
Víctor García, Santiago Escobar, Kazuhiro Ogata:
Modeling and verification of the post-quantum key encapsulation mechanism KYBER using Maude. FAVPQC@ICFEM 2022:
Duong Dinh Tran, Canh Minh Do, Santiago Escobar, Kazuhiro Ogata:
Hybrid Post-Quantum TLS formal specification in Maude-NPA – toward its security analysis. FAVPQC@ICFEM 2022
Raúl López-Rueda, Santiago Escobar:
Canonical Narrowing with Irreducibility and SMT Constraints as a Generic Symbolic Protocol Analysis Method. WRLA@ETAPS 2022
Raúl López-Rueda, Santiago Escobar, José Meseguer:
An Efficient Canonical Narrowing Implementation for Protocol Analysis. WRLA@ETAPS 2022
Canh Minh Do, Adrián Riesco, Santiago Escobar, Kazuhiro Ogata:
Parallel Maude-NPA for Cryptographic Protocol Analysis. WRLA@ETAPS 2022
2021
Thet Wai Mon, Dang Duy Bui, Duong Dinh Tran, Canh Minh Do, Kazuhiro Ogata:
Graphical Animations of the NS(L)PK Authentication Protocol. JVLC2021
Thet Wai Mon, Dang Duy Bui, Duong Dinh Tran, Kazuhiro Ogata:
Graphical Animations of the NSLPK Authentication Protocol. DMSVIVA 2021
Thet Wai Mon, Shuho Fujii, Duong Dinh Tran, Kazuhiro Ogata:
Formal verification of IFF and NSLPK authentication protocols with CiMPG. SEKE 2021