Congratulations to [Emanuele D'Osualdo](https://www.emanueledosualdo.com/) and Felix Stutz, (https://www.mpi-sws.org/people/fstutz/) whose paper, [Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions](https://drops.dagstuhl.de/opus/volltexte/2020/12843/pdf/LIPIcs-CONCUR-2020-31.pdf), has been accepted at this year’s [CONCUR](https://concur2020.forsyte.at/).
Congratulations to [Emanuele D'Osualdo](https://www.emanueledosualdo.com/) and [Felix Stutz](https://www.mpi-sws.org/people/fstutz/), whose paper, [Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions](https://drops.dagstuhl.de/opus/volltexte/2020/12843/pdf/LIPIcs-CONCUR-2020-31.pdf), has been accepted at this year’s [CONCUR](https://concur2020.forsyte.at/).
The paper explores the limits of what security properties can be proven by automatic analyses and aims at developing algorithms for proving security properties of cryptographic protocols automatically. Cryptographic protocols underpin everything on the internet nowadays: their goal is to establish secure communication in an insecure channel, through the use of cryptography. Despite being ubiquitous, they are very tricky to design. Indeed hackers exploit flaws in deployed protocols every day, with huge costs for individuals and society at large.