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