RSS Meetup

Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions

Sala 6.2.44, Ciências ULisboa

Por Emanuele D'Osualdo (MPI-SWS).

Cryptographic protocols underly absolutely everything we do on the internet, and yet they are riddled with flaws that are routinely exploited by hackers at great cost for society. Ideally, we would like to certify absence of flaws automatically, but the space of possible attacks is infinite and any verification problem becomes undecidable. We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied pi-calculus, with applications to automatic verification of stateful cryptographic protocols with unbounded sessions/nonces. Since the problem is undecidable in general, we introduce depth-bounded protocols, for which our decidable analysis is sound and complete. Our core contribution is a procedure to check that an invariant is inductive, which implies that every reachable configuration satisfies it. Our invariants can capture security properties like secrecy, can be inferred automatically, and represent an independently checkable certificate of correctness.

Bio: Emanuele D'Osualdo is a Postdoctoral Researcher at Max Planck Institute for Software Systems (MPI-SWS) in Saarbrücken, working on verification of concurrent software with Derek Dreyer. Until September 2020 he was a Marie Curie Fellow at Imperial College London, working with Philippa Gardner. Previously he worked with Prof. Roland Meyer at the University of Kaiserslautern.

His PhD thesis, supervised by Luke Ong at the University of Oxford, received the 2016 CPHC/BCS Distinguished Dissertation award as best of the UK. 

The focus of his research has been verification of concurrent systems using methods from separation logic, process algebra, types, model checking, automata, and static analysis.

RSS Meetups are monthly gatherings of LASIGE members with research interests mainly in Software Architecture, Verification, Testing, Programming Languages, Type Systems, Logic, Concurrency, and Formal Methods.

14h30
LASIGE Computer Science and Engineering Research Centre
Título e data do evento, com fotografia de cascas de ovo

Um evento que promete capacitar os participantes com conhecimentos e capacidades práticas sobre biomateriais.

Informações sobre o evento e fotografia do orador

Distinguished Talks @DI/LASIGE, por Tom Lenaerts (Université Libre de Bruxelles).

Título/data do evento e fotografia do orador

Seminário do Departamento de Engenharia Geográfica, Geofísica e Energia, por Vitor Rodrigues (LONGi Solar).

Seminário do Centro de Física Teórica e Computacional, por Susana Cardoso de Freitas (INESC Microsystems and Nanotechnologies and IST Universidade de Lisboa, Portugal).

Seminário de Tese (Doutoramento em Biodiversidade Genética e Evolução), por Mariya Kozak.

Mathematical Logic Seminar, por Bruno Dinis (Universidade de Évora).

Logótipo e data do evento

Jornadas de Química Tecnológica de Ciências ULisboa.

3.º Seminário Conjunto CFCUL / Rede Ibérica de Filosofia das Ciências, por Javier Anta (Universidade de Sevilha).

An action-packed event where you will have the opportunity to get to know the latest that is being made in Ciências, showcase your work and, above all, meet and discuss ideas with your department PhD colleagues! 

Conferência associada à exposição “A Porta do Pacífico: Uma viagem cartográfica pelo Estreito de Magalhães", por Suzana Nápoles (Centro de Matemática, Aplicações Fundamentais e Investigação Operacional - CMAFcIO).

Título do programa, sobre fundo colorido

Submissão de candidaturas até 30 de março de 2023.

Seminário Doutoral I (Doutoramento em Biologia), por Ana Sofia Laranjeira Lopes.

Título do projeto, sobre uma fotografia de região polar

Concurso para Projetos Exploratórios a decorrer até 31 de março de 2023.

Título do evento e fotografias de experiências científicas

Uma oportunidade única para alunos do 3.º ciclo conhecerem o mundo da Ciência de forma interativa e criativa.

Título do programa, sobre imagem alusiva à cibersegurança

This program aims to be the best international cybersecurity short/medium term course for executives and decision makers in Europe.

Logótipo do evento, sobre representação de Lisboa e Margem Sul do Tejo

This is a conference directed for Postdocs, PhD and Master students in Mathematics and affine areas of Lisbon Universities.

Logótipo do CEBiCNa, sobre um fundo branco

Concurso para atribuição de 20 bolsas de investigação, com candidaturas até 17 de abril de 2023.

Composição do logótipo da ULisboa e de representação do ser humano

A competição oferece aos estudantes de doutoramento da ULisboa a oportunidade de desenvolver novas competências de comunicação - candidaturas abertas de 03 a 17 de abril de 2023.

A feira de emprego da Faculdade de Ciências da Universidade de Lisboa.

Título do evento e fotografia de pessoa no topo de montanha

A 19 de abril de 2023 celebra-se o 112.º aniversário da Faculdade de Ciências da Universidade de Lisboa.

Conferência associada à exposição “A Porta do Pacífico: Uma viagem cartográfica pelo Estreito de Magalhães", por Joana Lima (Centro Interuniversitário de História das Ciências e da Tecnologia - CIUHCT).

Logótipo do evento, sobre um fundo branco

This year our motto is "Reinventing Science, for yourself and others”.

BioISI Research Seminar, por Margarida Gama-Carvalho (BioISI/Ciências ULisboa).

Páginas