Security protocols are short programs aiming at securing communications over a network. They are widely used in our everyday life. Their verification using symbolic models has shown its interest for detecting attacks and proving security properties. In particular, several automatic tools have been developed. However, the guarantees that the symbolic approach offers have been quite unclear compared to the computational approach that considers issues of complexity and probability. This later approach captures a strong notion of security, guaranteed against all probabilistic polynomial-time attacks.
In this course, we will first overview several techniques used for symbolically verifying security protocols. In a second part of the presentation, we will present recent results that aim at obtaining the best of both worlds: fully automated proofs and strong, clear security guarantees. The approach consists in proving that symbolic models are *sound* with respect to computational ones, that is, that any potential attack is indeed captured at the symbolic level.

Security APIs are Application Programming Interfaces to trusted systems such as cryptographic devices, online games, services on the web, etc. They should allow untrusted applications to access sensitive resources in a controlled way, e.g. signing a message using a cryptographic device without accessing the signature key, or modifying the status of an online game without cheating on the game rules. In practice, however, the flexibility required by these programming interfaces gives rise to attacks originated by 'unexpected' sequences of API invocation. It is possible, for example, to extract sensitive keys from PKCS#11 cryptographic tokens or guess a bank user PIN while it is checked inside a tamper-resistant Hardware Security Module, through a few suitable API calls to the device. In this course, we will review practical attacks on security APIs and we will introduce formal techniques to detect and fix them. We will describe Tookan, a tool that reverse engineers real cryptographic tokens and performs a formal analysis of the resulting model, finding possible attacks and testing them on the real device. We will finally show how to apply Tookan to break and fix a software simulator of a PKCS#11 token.

Type systems are effective tools for verifying the security of cryptographic protocols and implementations. They provide automation, modularity and scalability, and have been applied to large protocols. In this tutorial, I present and illustrate types for authenticity and secrecy, first using symbolic models for cryptography, then relying on computational assumptions:

1. We introduce refinement types (that is, types carrying formulas to record invariants) for programs written in F# and verified by F7, an SMT-based type checker.
2. We use types for declaring cryptographic invariants. We develop symbolic libraries for a range of cryptographic primitives, and we review a few case studies of protocol code.
3. We adapt our libraries to rely on standard computational assumptions. For each primitive, computational soundness follows from a code-based game-hopping argument in F#.

The tutorial is based on joint work with Karthik Bhargavan and Andy Gordon. Programming tools and examples are available here.