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

The course aims at enabling the participants to use different methods to measure the impacts of pollutants on ecosystems. Basic knowledge will be provided through theoretical and practical lessons on how to select and use the most suitable metrics based on the analysis of multiple compartments of the ecosystems.

Logótipo do CFTC, título e datas dos estágios

Three-weeks working on a project with a Researcher as a Supervisor, along with other workshops and activities - open to BSc or MSc students in Physics, Engineering Physics, Biomedical Engineering or other related fields.​

Título da iniciativa e fotografia do espaço

The program involves developing a research or science communication project under the supervision of researchers and science communicators from the Institute of Astrophysics and Space Sciences (IA). Two science communication workshops and a final seminar, in which the work developed is presented, are also part of the program.

Ação de formação para docentes, por Carlos Seco.

Título/data do evento e logótipos das entidades organizadoras

The program will consist of plenary lectures, oral, flash and poster communications, and a round table about “Science beyond academia: entrepreneurship” - registration is mandatory but free of charge!

This course offers an overview of the different ways to measure biodiversity, and provides tips for the stratification of primary biodiversity data and the construction of variables that describe its various facets. It also includes an in-depth review of the different types of data used to measure biodiversity and their problems and limitations.

Logótipo do evento

The most important international scientific meeting on the theory and applications of stochastic processes.

The goal of this course is to provide participants with current and practical knowledge on urban ecology, including its ecological and social aspects.

Logótipo do programa e fotografias de jovens investigadores

Candidata-te até 23 de junho e vem investigar connosco!

Placa de circuito

4.ª edição do Prémio de Inovação IN3+, com candidaturas até 31 de julho de 2023.

Sediment continuum: applying an integrated management approach.

Vista aérea da Estação Experimental de Moluscicultura de Tavira (EEMT)

EDUCOAST Summer School 2023, com candidaturas até 07 de junho de 2023.

RUTTER training school - new deadline for registration: 15 May 2023.

Título, data e localização do evento

The EU PVSEC is the largest international Conference for Photovoltaic research, technologies and applications and at the same time a PV Industry Exhibition, where specialized PV Industry presents technologies, innovations and new concepts in the upstream PV sector.

Páginas