Update 2020-08-31-concur2020.md

_posts/2020-08-31-concur2020.md

@@ -6,6 +6,6 @@ Congratulations to [Emanuele D'Osualdo]( https://www.emanueledosualdo.com/) and
 
 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. 
 
-In the paper, they 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, the authors introduce depth-bounded protocols, a strict generalisation of a class from the literature, for which our decidable analysis is sound and complete. Their core contribution is a procedure to check that an invariant is inductive, which implies that every reachable configuration satisfies it. Their invariants can capture security properties like secrecy, can be inferred automatically, and represent an independently checkable certificate of correctness. They also provide a prototype implementation and report on its performance on some textbook examples. The [extended technical report](https://arxiv.org/abs/1911.05430) is also available on [this link](https://arxiv.org/abs/1911.05430).
+In the paper, the authors 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, the authors introduce depth-bounded protocols, a strict generalisation of a class from the literature, for which our decidable analysis is sound and complete. Their core contribution is a procedure to check that an invariant is inductive, which implies that every reachable configuration satisfies it. Their invariants can capture security properties like secrecy, can be inferred automatically, and represent an independently checkable certificate of correctness. They also provide a prototype implementation and report on its performance on some textbook examples. The [extended technical report](https://arxiv.org/abs/1911.05430) is also available on [this link](https://arxiv.org/abs/1911.05430).
 
 CONCUR 2020, the [31st International Conference on Concurrency Theory](https://drops.dagstuhl.de/opus/portals/lipics/index.php?semnr=16161) will take place online on 1-4 September 2020.