Cryptography
Florian Kerschbaum (University of Waterloo)
Security and Privacy in Data Science
Data science is the process from collection of data to the use of new insights gained from this data. It is at the core of the big data and machine learning revolution fueling the digitization of our economy. The integration of data science and machine learning into digital and cyber-physical processes and the often sensitive nature of personally identifiable data used in the process, expose the data science process to security and privacy threats. In this talk I will review three exemplary security and privacy problems in different phases of the data science lifecycle and show potential countermeasures. First, I will show how to enhance the privacy of data collection using secure multi-party computation and differential privacy. Second, I will show how to protect data outsourced to a cloud database system and still perform efficient queries using keyword PIR and homomorphic encryption. Last, I will show that differential privacy does…
Charlie Jacomme (CISPA)
Not so AdHoc testing: formal methods in the standardization of the EDHOC protocol
Abstract: We believe that formal methods in security should be leveraged in all the standardisation's of security protocols in order to strengthen their guarantees. To be effective, such analyses should be:
* maintainable: the security analysis should be performed on every step of the way, i.e. each iteration of the draft;
* pessimistic: all possible threat models, notably all sort of compromise should be considered;
* precise: the analysis should notably include as many real life weaknesses of the concrete cryptographic primitives specified.
In this talk, we illustrate how such a goal may be approached by detailing our analysis of the current IETF draft standard of the EDHOC protocol, as well as our subsequent interactions with its LAKE working group.
We will proceed in three steps, first introducing the Sapic+ platform that allows from a single modeling of a protocol to benefit from all the capabilities of multiple automated verification tools (ProVerif,Tamarin,DeepSec). We will then introduce multiple recent advances on how to better model the cryptographic primitives and their real life weaknesses. We will finally show how we leveraged Sapic+ along with the advanced primitive models to analyze the EDHOC protocol and provide feedback to the LAKE working group that has been integrated in latter drafts.
François Dupressoir (University of Bristol)
EasyCrypt in anger — Proofs for Primitives, Constructions and Protocols
The EasyCrypt proof assistant offers—in a single tool—the ability to reason about cryptographic security at various scales from primitives to protocols. However, this flexibility comes at a huge cost in usability. This talk will discuss insights gained through the recent formalisation of primitives (SHA-3, XMSS), constructions (KMS, crypto_box) and protocols (distance-bounding, AKE) and explore plans for improvements to the tool that would enable its use on larger protocols, and for the creation of beginner-friendly tutorial material that would enable it to be used more broadly.