Conferencia de Santiago Escobar Román
Métodos Formales para el análisis de protocolos criptográficos
Categoría: I+D+i UMA
PONENTE: Dr. Santiago Escobar Román, docente de la Universitat Politècnica de València.
FECHA: Miércoles, 09 de noviembre de 2022, 16:00
LUGAR: Sala de grados A y online en el enlace https://eu.bbcollab.com/guest/6e55a0e777884601aacdfb4f887c93c3
ASIGNATURA: Métodos para la Construcción de Software Fiable
TÍTULO: Métodos Formales para el análisis de protocolos criptográficos.
RESUMEN: En esta charla, se proporciona una visión general de los aspectos teóricos y prácticos del analizador de protocolos Maude-NPA. Es una herramienta para el análisis de protocolos criptográficos. Busca hacia atrás a partir de un patrón que define las propiedades de confidencialidad, autenticación o indistinguibilidad de un protocolo y es capaz de encontrar una instancia o probar la ausencia de cualquier instancia. Maude-NPA está diseñado para tener en cuenta las propiedades algebraicas de los sistemas criptográficos involucrados (por ejemplo, ó exclusivo, Diffie-Hellman, homomorfismos, etc.) para brindar una representación más completa tanto del protocolo como de las capacidades de los atacantes. Durante el desarrollo de la herramienta también hemos definido nuevos marcos teóricos y prácticos como la unificación basada en variantes, la verificación de modelos lógicos, la unificación asimétrica o las optimizaciones del espacio de estados.
BIOGRAFÍA: Santiago Escobar es Titular de Universidad de la Universitat Politècnica de València desde 2010. Es Doctor en Informática por la Universitat Politècnica de València desde 2003. Ha dirigido cinco tesis doctorales y dos en marcha. Ha publicado más de 90 artículos de revista y congresos. Ha participado en más de 50 comités científicos de congresos. Ha sido el presidente del comité científico en más de 10 ocasiones. Ha impartido más de 50 charlas invitadas en centros de investigación, congresos y escuelas internacionales. Ha realizado varias estancias de investigación en Europa y EE.UU. (algunas de ellas de hasta seis meses).
Sus intereses incluyen cybersecurity, security science, and provable security. Se destacan los siguientes puntos:
- Ha desarrollado el analizador de protocolos criptográficos Maude-NPA desde 2004 en colaboración con Catherine Meadows de la Marina de EE.UU. en Washington D.C. y Jose Meseguer del Information Trust Institute de la University of Illinois at Urbana-Champaign. Algunas invenciones de Maude-NPA son parte actualmente de otros analizadores de protocolos, como Tamarin del ETH Zurich en Suiza, CPSA del MITRE en EE.UU. o AKISS del INRIA en Francia.
- Es parte del equipo de desarrollo del lenguaje de programación Maude desde 2007. Este lenguaje es desarrollado por SRI International en Palo Alto, CA, EE.UU. Maude es utilizado de forma habitual por la NASA, Microsoft o Boeing para el modelado, análisis y verificación de propiedades de seguridad.
- Es subdirector para informática de la Cátedra STADLER de la Universitat Politècnica de València. Stadler Rail está presente en España desde el 1 de enero de 2016, cuando la empresa Suiza compró las instalaciones de Albuixech, Valencia, que fueron parte anteriormente de MACOSA, la francesa Alstom y la alemana Vossloh. Ha colaborado con Stadler desde 2016 en diferentes aspectos relacionados con ciberseguridad.
- Ha colaborado desde 2019 con la empresa de ciberseguridad Nunsys del Parque Tecnológico de Paterna.
- Ha empezado a colaborar con la empresa Laberit de Valencia y la empresa DEKRA de Málaga.
- Colabora con (i) el NASA Langley Research Center en Hampton, VA, USA, (ii) SRI International, Palo Alto, CA, USA, (iii) ETH Zurich, Suiza, (iv) Pohang University of Science and Technology, Corea, y (v) Universidad de Oslo, Noruega.
Para más información: http://personales.upv.es/sanesro
.