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

Seminário do Laboratório de Instrumentação e Física Experimental de Partículas, por Pedro Cruz (Northeastern University).

Apresentação dos trabalhos desenvolvidos no âmbito do programa Estágios de Verão CEAUL - Sê Investigador.

Logótipo do EVM 2024

Por Giosuè Muratore (DM Ciências ULisboa e CMAFcIO).

Título do programa, sobre mosaico de fotografias de jovens cientistas

As candidaturas encontram-se encerradas. Obrigada aos quase 80 candidatos/as!

Logótipo do EVM 2024

Por Pedro Duarte (DM Ciências ULisboa, CMAFcIO).

Logótipo do EVM 2024

Por Maria Manuel Torres (DM Ciências ULisboa e CMAFcIO).

Fotografia de ilha

Seminários Doutorais no âmbito da disciplina de Projeto de Investigação (Doutoramento em Ciências do Mar).

Seminário do Centro de Matemática, Aplicações Fundamentais e Investigação Operacional, por Baptiste Claustre (aluno ENS Lyon, estagiário CMAFcIO).

Logótipo do EVM 2024

Por: Jorge Buescu (DM Ciências ULisboa e CMAFcIO).

Titulo e data do evento, com imagem de ponte sobre o tejo

Um evento organizado no âmbito da Ação COST EURO-MIC, de cujo Comitê de Gestão Elisabete Silva, líder do Bioactive and Multifunctional Materials Lab do BioISI, faz parte.

Logótipo do EVM 2024

Por Jean-Baptiste Casteras (DM Ciências ULisboa e CMAFcIO).

Chegou a hora: os participantes do Programa Ser Cientista vão apresentar os projetos que desenvolveram ao longo de uma semana, acompanhados por docentes e investigadores de CIÊNCIAS. E todos podem assistir!

Imagem do evento

Extended enrolement date until July 12th.

Logótipo do evento, sobre um fundo branco

Um evento de reunião da comunidade nacional nas diversas vertentes da informática, com a ambição de ser o fórum de eleição para a divulgação, discussão e reconhecimento de trabalhos científicos.

Are you ready for this year's edition?

Imagem do evento - título, local e data do evento

Investigação Ecológica ao Serviço da Conservação

A leading venue for presenting and discussing the latest research, industrial practice and innovations in dependable and secure computing.