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
Fotografia de Chapim-azul

The goal of this course is to provide the participants with the most recent and practical knowledge on the use of Functional Diversity.

O evento reunirá alunos de Ciências ULisboa e do ISCAL, proporcionando-lhes uma oportunidade única para apresentarem e defenderem os seus projetos empreendedores num formato de pitch.

Seminário do Centro de Física Teórica e Computacional, por Susana Barbosa (INESC TEC, Porto, Portugal).

Logótipo CQE Days 2025

O encontro tem como objetivo divulgar e promover os resultados da investigação produzidos nos dois pólos do Centro de Química Estrutural (CIÊNCIAS e IST), estimulando a criatividade, o trabalho interdisciplinar e o espírito científico.

Palestra de divulgação das atividades e oportunidades do IEEE (Institute of Electrical and Electronics Engineers).

Seminário de Lógica Matemática, por Eduardo Magalhães (Universidade do Porto).

Mão a segurar em globo de vidro

Curso acreditado pelo CCPFC para efeitos de progressão na carreira dos professores na dimensão cientifico-pedagógica dos grupos 230, 420, 510, 520 e 560, com candidaturas até 30 de abril.

Seminário de Geometria e Física, por Tomás Inácio (FCUL, Universidade de Lisboa).

The aim of this event is to illustrate the importance of interdisciplinarity. To do so the meeting will bring together researchers from different areas who work in interdisciplinary fields within Ciências ULisboa

Cardume

Seminário Doutoral I (Doutoramento em Biologia), por Eduardo Miguel Onofre Feijão.

Seminário do Departamento de Física de Ciências ULisboa, por José Manuel Rebordão (FCUL - DF).

Seminário de Análise e Equações Diferenciais, por João Pedro Ramos (Instituto Nacional de Matemática Pura e Aplicada).

Logótipo do LIP Summer Internship Program

Um programa destinado a estudantes de Física e Engenharia com interesse em investigação científica e tecnológica, com candidaturas até 15 de maio (nova data).

“Coroa de Flores” cósmica

Seminário do Instituto de Astrofísica e Ciências do Espaço, por Federica Loiacono (INAF OAS Bologna, Italy).

Seminário do Centro de Física Teórica e Computacional, por João Amaral (Department of Physics and CICECO, University of Aveiro, Portugal).

Seminário de Análise e Equações Diferenciais, por Wladimir Neves (Universidade Federal do Rio de Janeiro).

Título/data/local do evento, logótipos das entidades organizadoras e fotografia de peixe

The event aims to facilitate the exchange of information and knowledge among professionals to advance the understanding, collaboration and capabilities of aquaculture to respond to the impact of climate change in a rapidly changing global environment.

Composição do logótipo da ULisboa e de representação do rosto humano à base de relógios

22 de maio - dois dos doze finalistas da competição são alunos de CIÊNCIAS.

Seminário de Análise e Equações Diferenciais, por Leonid Berlyand (Penn State University).

Seminário do Instituto de Astrofísica e Ciências do Espaço, por Pier-Stefano Corasaniti (Observatoire de Paris-Meudon, France).

Uma oportunidade única para interagir com a comunidade global de computação científica.

Logótipo Moodle

Ação de formação para docentes e investigadores de CIÊNCIAS.

Logótipo Mentimeter

Ação de formação para docentes e investigadores de CIÊNCIAS.

Título/data/local do evento e iconografia representativa de energias renováveis

Inscrições até 16 de maio! Junta-te a esta revolução energética e faz a diferença!

Neste curso ficarás a saber como te podes tornar um permacultor eficiente, produtivo e consciente! O curso está preparado para iniciantes na prática de permacultura.

Páginas