Publications - Protocol Verification (Security)
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)
Available:
DOI
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 Computer Science, volume 9, e1556, 2023.
Available:
DOI
-
-
Víctor García, Santiago Escobar, Kazuhiro Ogata, Sedat Akleylek, Ayoub Otmani.
Modelling and verification of post-quantum key encapsulation mechanisms using Maude.
PeerJ Computer Science, volume 9, e1547, 2023.
Available:
DOI
-
-
Daniel Galán, Víctor García, Santiago Escobar, Catherine Meadows, and Jose Meseguer.
Protocol Dialects as Formal Patterns.
In Proceedings of
28th European Symposium on
Research in Computer Security (ESORICS 2023),
September 25-29, 2023, The Hague, The Netherlands.
Lecture Notes in Computer Science, volume 14345, pages 42-61.
© Springer-Verlag
Available:
DOI
-
-
Fan Yang, Santiago Escobar, Catherine A. Meadows, José Meseguer, Sonia Santiago
Strand Spaces with Choice via a Process Algebra Semantics.
In Proceedings of
Essays Dedicated to Manuel Hermenegildo on the Occasion of His 60th Birthday,
Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems.
Lecture Notes in Computer Science, volume 13160, pages 307-350.
© Springer-Verlag
Available:
DOI
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.
In Proceedings of the International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols,
co-located with
the 23rd International Conference on Formal Engineering Methods (ICFEM 2022),
Madrid, Spain, October 24, 2022.
CEUR Workshop Proceedings,
volume 3280,
pages 16-31,
CEUR-WS.org 2022
Available:
DOI
-
-
Víctor García, Santiago Escobar, Kazuhiro Ogata
Modeling and verification of the post-quantum key encapsulation mechanism KYBER using Maude.
In Proceedings of the International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols,
co-located with
the 23rd International Conference on Formal Engineering Methods (ICFEM 2022),
Madrid, Spain, October 24, 2022.
CEUR Workshop Proceedings,
volume 3280,
pages 32-49,
CEUR-WS.org 2022
Available:
DOI
-
-
Duong Dinh Tran, Canh Minh Do, Santiago Escobar, Kazuhiro Ogata
Hybrid Post-Quantum TLS formal specification in Maude-NPA - toward its security analysis.
In Proceedings of the International Workshop on Formal Analysis and Verification of Post-Quantum Cryptographic Protocols,
co-located with
the 23rd International Conference on Formal Engineering Methods (ICFEM 2022),
Madrid, Spain, October 24, 2022.
CEUR Workshop Proceedings,
volume 3280,
pages 50-64,
CEUR-WS.org 2022
Available:
DOI
-
-
Canh Minh Do, Adrián Riesco, Santiago Escobar, and Kazuhiro Ogata.
Parallel Maude-NPA for Cryptographic Protocol Analysis.
In Kyungmin Bae (ed),
14th International Workshop on Rewriting Logic and Its Applications,
WRLA 2022.
Lecture Notes in Computer Science, volume 13252, pages 253--273.
© Springer-Verlag
Available:
DOI
-
-
Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, and Ayoub Otmani.
Formal specification and model checking of lattice-based key encapsulation mechanisms in Maude.
In Kyungmin Bae (ed),
14th International Workshop on Rewriting Logic and Its Applications,
WRLA 2022.
-
-
Duong Dinh Tran, Kazuhiro Ogata, Santiago Escobar, Sedat Akleylek, and Ayoub Otmani.
Formal specification and model checking of Saber lattice-based key encapsulation mechanism in Maude.
In 34th International Conference on
Software Engineering & Knowledge Engineering (SEKE 2022).
KSIR Virtual Conference Center, Pittsburgh, USA.
Available:
DOI
2021
-
-
Damián Aparicio-Sánchez,
Santiago Escobar,
Catherine Meadows,
Jose Meseguer,
Julia Sapiña.
Protocol Analysis with Time and Space.
In: Dougherty D., Meseguer J., Mödersheim S.A., Rowe P. (eds) Protocols, Strands, and Logic.
Lecture Notes in Computer Science, vol 13066, pp 22-49, 2021.
© Springer-Verlag
Available:
DOI
2020
-
-
Damián Aparicio-Sánchez,
Santiago Escobar,
Catherine Meadows,
Jose Meseguer,
Julia Sapiña.
Protocol Analysis with Time.
In proceedings of
21st International Conference on Cryptology in India.
Lecture Notes in Computer Science, volume 12578, pages 128-150. 2020
© Springer-Verlag
Available:
DOI
-
-
Damián Aparicio-Sánchez,
Santiago Escobar,
Raúl Gutiérrez,
Julia Sapiña.
An Optimizing Protocol Transformation for Constructor Finite Variant Theories in Maude-NPA.
In proceedings of
25th European Symposium on Research in Computer Security (ESORICS) 2020.
Lecture Notes in Computer Science, volume 12309, pages 230-250. 2020
© Springer-Verlag
Available:
DOI
2019
-
-
Catherine Meadows, Santiago Escobar, Jose Meseguer.
Maude-NPA and Formal Analysis of Protocols with Equational
Theories.
NATO Science for Peace and Security Series - D: Information and
Communication Security.
Volume 53: Engineering Secure and Dependable Software Systems,
pages 163-188, 2019.
© IOS Press
Available:
IOS link-
DOI
2018
-
-
Antonio González-Burgueño, Damián Aparicio-Sánchez, Santiago Escobar, Catherine Meadows, and José Meseguer.
Formal verification of the YubiKey and YUbiHSM APIs in Maude-NPA.
In proceedings of
22th International Conferences on Logic for Programming, Artificial
Intelligence and Reasoning (LPAR18),
Awassa Ethiopia, 16-21 November 2018.
EPiC
Series in Computing, volume 57, pages 400-417.
Available:
DOI
EPiC Series in Computing
CoRR
-
-
Fan Yang, Santiago Escobar, Catherine Meadows, José Meseguer.
Modular Verification of Sequential Composition for Private Channels in Maude-NPA.
In proceedings of
14th International Workshop on Security and Trust Management
(STM 2018).
Lecture Notes in Computer Science, volume 11091, pages 20-36.
© Springer-Verlag
Available:
DOI
2016
-
-
Fan Yang, Santiago Escobar, Catherine Meadows, José Meseguer,
and Sonia Santiago.
Strand Spaces with Choice via a Process Algebra Semantics.
In proceedings of
18th International Symposium on
Principles and Practice of Declarative Programming
(PPDP 2016).
© ACM Press
Available:
DOI
2015
-
-
Santiago Escobar, Catherine Meadows, José Meseguer, Sonia Santiago.
Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories.
In proceedings of
Programming Languages with Applications to Biology and Security - Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday.
Lecture Notes in Computer Science, volume 9465, pages 238-261.
Springer 2015.
© Springer-Verlag
Available:
DOI
-
-
Antonio González-Burgueño, Sonia Santiago, Santiago Escobar, Catherine Meadows, and José Meseguer.
Analysis of the PKCS#11 API using the Maude-NPA tool.
In proceedings of
2nd International Conference on Research in Security Standardisation (SSR 2015).
Lecture Notes in Computer Science, volume 9497, pages 86-106.
Springer 2015.
© Springer-Verlag
2014
-
-
Antonio González-Burgueño, Sonia Santiago, Santiago Escobar, Catherine Meadows, and José Meseguer.
Analysis of the IBM CCA Security API Protocols in Maude-NPA.
In proceedings of
1st International Conference on Research in Security Standardisation (SSR 2014),
Royal Holloway, London, UK - December 16-17, 2014
Lecture Notes in Computer Science, volume 8893, pages 111-130,
Springer 2014.
© Springer-Verlag
Available:
Preliminary version
DOI
-
-
Sonia Santiago, Santiago Escobar, Catherine Meadows, and José Meseguer.
A Formal Definition of Protocol Indistinguishability and its Verification Using Maude-NPA.
In proceedings of
10th International Workshop on Security and Trust Management (STM 2014)
in conjunction with ESORICS 2014.,
Wrocław, Poland - September 10-11, 2014
Lecture Notes in Computer Science, volume 8743, pages 162-177,
Springer 2014.
© Springer-Verlag
Available:
Preliminary version
DOI
-
-
Fan Yang, Santiago Escobar, Catherine Meadows, José Meseguer,
and Paliath Narendran.
Theories of Homomorphic Encryption, Unification, and the Finite Variant Property.
In proceedings of
16th International Symposium on
Principles and Practice of Declarative Programming
(PPDP 2014),
September 8-10, 2014, Canterbury, UK
© ACM Press
Available:
Preliminary version
-
-
Sonia Santiago, Santiago Escobar, Catherine Meadows, and José Meseguer.
A Rewriting-based Forwards Semantics for Maude-NPA.
In proceedings of
Symposium and Bootcamp on the Science of Security (HotSoS 2014),
April 8-9, 2014, Raleigh, NC, USA.
ACM Digital Library,
2014.
© ACM Press
Available:
DOI
Preliminary version
-
-
Santiago Escobar,
Catherine Meadows,
José
Meseguer,
Sonia Santiago
State Space Reduction in the Maude-NRL Protocol Analyzer.
Information and Computation,
Volume 238, November 2014, Pages 157-186.
© Elsevier
Available:
Preliminary
version
DOI
2013
-
-
Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, José Meseguer, Paliath Narendran, Sonia Santiago, and Ralf Sasse.
Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis
In proceedings of
CADE-24 - the 24th International
Conference on Automated Deduction,
Lecture Notes in Computer Science, volume 7898, pages 231-248,
Springer 2013.
© Springer-Verlag
Available:
Preliminary version
DOI
2012
-
-
Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, José Meseguer, Paliath Narendran, Sonia Santiago, and Ralf Sasse.
Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions
In proceedings of
17th European Symposium
on Research in Computer Security (ESORICS 2012).,
Lecture Notes in Computer Science, volume 7459, pages 73-90, 2012.
© Springer-Verlag
Available:
DOI
-
-
Serdar Erbatur, Santiago Escobar, and Paliath Narendran.
Unification modulo a property of the El Gamal Encryption Scheme.
In proceedings of
The International Workshop on Unification (UNIF 2012).
Available:
Preliminary version
2011
-
-
Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu,
Christopher Lynch, Catherine Meadows, Jose Meseguer, Paliath
Narendran and Ralf Sasse.
Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis
In proceedings of
The International Workshop on Unification (UNIF 2011).
-
-
Santiago Escobar,
Deepak Kapur,
Christophe Lynch,
Catherine Meadows,
José
Meseguer,
Paliath Narendran,
and
Ralf Sasse.
Protocol Analysis in Maude-NPA Using Unification Modulo Homomorphic Encryption
In proceedings of
13th International ACM SIGPLAN Symposium on
Principles and Practice of Declarative Programming (PPDP'2011).
© ACM Press
Available:
DOI
-
-
Ralf Sasse,
Santiago Escobar,
Catherine Meadows,
José
Meseguer.
Protocol Analysis Modulo Combination of Theories: A Case Study in Maude-NPA.
In proceedings of
6th International Workshop on Security and Trust Management (STM'10),
Lecture Notes in Computer Science, Volume 6710, pages 163-178, 2011.
© Springer-Verlag
Available:
DOI
PDF
2010
-
-
S. Escobar,
C. Meadows,
J. Meseguer
S. Santiago
Sequential Protocol Composition in Maude-NPA
In proceedings of
European Symposium on Research in Computer Security (ESORICS 2010),
LNCS 6345, pages 303-318. 2010.
© Springer-Verlag
Available:
DOI
2009
-
-
S. Santiago,
C. Talcott, S. Escobar,
Catherine Meadows,
J. Meseguer
A Graphical User Interface for Maude-NPA.
In IX Jornadas sobre ProgramaciĆ³n y Lenguajes (PROLE 2009).
Electronic Notes in Theoretical Computer Science,
volume 258, number 1, pages 3-20. Elsevier, 2009.
© Elsevier
Available:
DOI
-
-
Santiago Escobar,
Catherine Meadows,
José Meseguer.
Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties.
FOSAD 2007/2008/2009 Tutorial Lectures,
LNCS 5705, pages 1-50.
© Springer-Verlag
Available:
PDF
2008
-
-
Santiago Escobar,
Catherine Meadows,
José Meseguer.
The Maude-NRL Protocol Analyzer (short paper)
In proceedings of
15th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR08), Doha, Qatar.
-
-
Santiago Escobar,
Catherine Meadows,
José Meseguer.
State Space Reduction in the Maude-NRL Protocol Analyzer
In proceedings of
13th European Symposium on Research in Computer Security (ESORICS08),
LNCS 5283, pages 548-562, 2008.
© Springer-Verlag
Available:
DOI
PDF
-
-
Santiago Escobar,
Catherine Meadows,
José Meseguer.
The Maude-NRL Protocol Analyzer (short paper)
In LICS-CSF short papers
21st IEEE Computer Security Foundations Symposium (CSF)
and
23rd IEEE Symposium on Logic in Computer Science (LICS).
, Pittsburgh, USA.
2007
-
-
Santiago Escobar,
Joe Hendrix,
Catherine Meadows,
José Meseguer.
Diffie-Hellman Cryptographic Reasoning in the Maude-NRL Protocol Analyzer
In informal proceedings of
2nd
International Workshop on Security and Rewriting Techniques (SecReT 2007),
2007.
Available:
PDF
2006
-
-
Santiago Escobar,
Catherine Meadows,
José Meseguer.
A Rewriting-Based Inference System for the NRL Protocol Analyzer and its Meta-Logical Properties
Theoretical Computer Science,
Volume 367, Issues 1-2, pages 162-202.
Extended and revised version of this paper.
© Elsevier
Available:
DOI link
Preliminary version
-
-
Santiago Escobar,
Catherine Meadows,
José Meseguer.
The Maude-NRL Protocol Analyzer: A Rewriting-Based Inference System for Equational Cryptographic Reasoning (extended abstract)
In proceedings of
Midwest Security Workshop (MSW'2006),
Urbana, IL, USA. 2006.
-
-
Santiago Escobar,
Catherine Meadows,
José Meseguer.
The Maude-NRL Protocol Analyzer: A Rewriting-Based Inference System for Equational Cryptographic Reasoning
(extended abstract)
In proceedings of
VI Jornadas sobre ProgramaciĆ³n y Lenguajes (PROLE'2006),
2006.
-
-
Santiago Escobar,
Catherine Meadows,
José Meseguer.
Equational Cryptographic Reasoning in the Maude-NRL Protocol Analyzer
In proceedings of
1st
International Workshop on Security and Rewriting Techniques (SecReT 2006),
Electronic Notes in Theoretical Computer Science,
volume 171, pages 23-36, 2007.
© Elsevier
Available:
DOI link
PDF
2005
-
-
Santiago Escobar,
Catherine Meadows,
José Meseguer.
A Rewriting-Based Inference System for the NRL Protocol Analyzer: Grammar Generation
In proceedings of
3rd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE'05),
pages 1-12, 2005.
© ACM Press
Superseded by this journal publication.
Available:
ACM link
PDF
Last modified: Sep 22 2023