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/data do evento e fotografias dos oradores

Masterclass do Tec Labs.

Seminário do Departamento de Engenharia Geográfica, Geofísica e Energia, por Vera Correia (Direção Técnica - EGF).

Fotografia de folhas de plantas

Seminário Doutoral II (Doutoramento em Biologia de Ciências ULisboa).

Título do evento sobre fotografia, em contraluz, representativa de ex-alunos da ULisboa

Gostaria de saber mais sobre a Associação Alumni ULisboa? Ouvir e partilhar experiências de outras associações Alumni?

Logótipo do projeto e fotografia do orador da sessão inaugural

António Raminhos abre o Ciências em Harmonia.

Seminário do Departamento de Física de Ciências ULisboa, por Luís Ducla Soares (Instituto de Telecomunicações & ISCTE-IUL).

Colóquio de Matemática, por Mário Edmundo (FCUL - DM).

Cartaz do evento

Reasoning Seminar, por João Alberto Pinto (Universidade do Porto).

Seminário Doutoral II (Doutoramento em Biologia), por Marta Maria Alves Antunes

Logótipo do evento, sobre um fundo verde

A grande festa da Ciência está de volta ao MUHNAC!

CELab PhD Seminar, por Earl K. Miller (The Picower Institute for Learning and Memory and Department of Brain and Cognitive Sciences, MIT).

Logótipo do projeto

A 19.ª edição do projeto decorre no 1.º semestre de 2023/2024 - inscrições até 30 de setembro.

Título do evento e representação de dois peixes

Este curso intensivo, com duração de uma semana (36 horas) e inscrições até 04 de outubro, tem como objetivo aprofundar o conhecimento sobre as comunidades de peixes existentes nos ecossistemas fluviais portugueses.

Título/prazo da iniciativa e logótipo do Ciências Research and Innovation Day

Participe até 10 de outubro / Submit you application until 10 October.

Logótipo do prémio, sobre um fundo branco

As candidaturas à 20.ª edição decorrem até 10 de outubro.

Ilustração de peixe, por Pedro Salgado

Por Pedro Salgado (Biólogo, Ilustrador Científico. Professor Especialista - ilustração).

Luís Saraiva (Ciências ULisboa) é o coordenador nacional do Seminário Nacional de História da Matemática.

Join us on 24 October 2023 for the 5th edition of Ciências Research & Innovation Day! A public showcase of the best science made in this centenary institution.

Título/data do evento e fotografia de parque eólico

Um fórum de discussão e reflexão sobre os mais recentes avanços na investigação, inovação e práticas na implementação dos Objetivos do Desenvolvimento Sustentável nas Instituições de Ensino Superior em Portugal e nos países da lusofonia.

EAP-II tem como objetivo fomentar um espaço de partilha de conhecimento entre a comunidade científica e não-científica, de uma forma simples e acessível para todos.

Título, local e data do evento, acompanhados da representação de um cavalo-marinho e das típicas chaminés algarvias

A conservação da biodiversidade em Portugal deve sair do papel e rumar a ações que promovam, no território, o normal funcionamento dos ecossistemas, para garantir o desenvolvimento sustentável, do ponto de vista ecológico e ser aceite do ponto de vista social. Urge integrar o conhecimento gerado pelos ecólogos de forma a que estes possam responder oportuna e corretamente, quando chamados a intervir.

Fotografia de investigadores em contexto laboratorial

Novo prazo de candidatura: 01 a 30 de novembro de 2023.