diff --git a/_posts/2018-07-16-seminar.md b/_posts/2018-07-16-seminar.md new file mode 100644 index 0000000000000000000000000000000000000000..194408813ab2b70e58186471216281f18d2444b1 --- /dev/null +++ b/_posts/2018-07-16-seminar.md @@ -0,0 +1,20 @@ +--- +title: Seminar by Felix Stutz on Automated Verification of Security Protocols +--- +Felix Stutz gave a talk on Monday on Automated Verification of Security Protocols. +This work is part of the project he is doing with Emanuele D’Osualdo and will +inform his Master Thesis. +The abstract is: +Security protocols are distributed programs that are designed to achieve secure +communications using cryptography. A distinctive feature of the security properties +of protocols is that they must hold in the presence of an active adversarial +environment, and this makes them challenging to verify. An important example +of such a security property is secrecy: can the protocol leak a (secret) message +to the environment as a result of interference by the intruder? +This project's goal is to develop a new algorithm to verify secrecy of cryptographic +protocols with unbounded sessions and nonces. +The novelty of the approach, based on a new decidability result +by [D'Osualdo et al.(CSF17)](http://psvg.doc.ic.ac.uk/publications/DOsualdo2017Deciding.html), +is in how the unboundedness caused by the use of unlimited nonces can be tamed +algorithmically. We will present a new verification algorithm for secrecy based +on symbolic representations of inductive invariants of protocols. \ No newline at end of file