Course meeting times
- Wednesdays at 14-16, Δ-2039
- Wednesdays at 16-18, Δ-2039
According to studies information system, we should have a lecture first and a practice session afterwards. In practice, we will not really make such a distinction.
We will try to use the cameras present in the lecture rooms in Δ to enable the lectures to be followed remotely and stored on University of Tartu's BigBlueButton. Or we will set up Zoom sessions, which we will also record. Still, please make effort to attend the lectures in person.
Instructors
- Peeter Laud,
peeter.laud@cyber.ee - Alisa Pankova,
alisa.pankova@cyber.ee - Pille Pullonen-Raudvere,
pille.pullonen-raudvere@cyber.ee
Content of the course
The content of the course is going to be somewhat different much from two years ago, when this course was last given. As there is now a separate course on Zero-Knowledge protocols offered, we will not cover them in great detail any more. Instead, we will go more deeply into the formal verification of protocols.
Key-exchange protocols
- Specifying and modelling protocols. What does it mean to satisfy confidentiality / integrity properties? What properties are wanted? Symbolic model of cryptography. Some examples of protocols.
- More "advanced" properties, e.g. forward secrecy, anonymity, resistance to offline guessing attacks, resistance to DoS attacks. Observational equivalences.
- TLS (need to cover some options there, e.g. client-side certificates) and SmartID. Perhaps we'll also separately look at the Mobile-ID protocol.
- Tools for proving protocol properties. ProVerif and Tamarin. We may also look into other tools (DeepSec, GSVerif, VerifPal) that are more tailored towards certain kinds of properties or protocols.
- Perhaps we will also look into CryptoVerif: a tool that works in the computational model
- Relationship between symbolic and computational models.
Secure Multiparty Computation (SMC)
- Security definitions for passively secure multiparty computation protocols.
- Garbled circuits. Oblivious transfer (OT) and OT extension. Security proof in symbolic model. Tricks for reducing the communication (Free-XOR, garbled row reduction, half-gates)
- Other ways for passively secure SMC. GMW. OT-extension. Linear secret sharing schemes (Shamir's scheme, additive sharing, replicated sharing) and multiplicative LSSS. Threshold homomorphic encryption. The general idea of pre-computed multiplication triples.
- Definitions and the like for active security. Also cover some intermediate-strength properties like covert security and active-security-with-abort.
- Protocols for broadcast. Byzantine agreement. Will perhaps do a short excursion towards blockchains (to put things into context and so that students understand that many blockchain technologies are actually Byzantine agreement protocols).
- Actively secure schemes from verifiable secret sharing.
- Theory: cannot have information-theoretically secure Byzantine agreement, if 1/3 of all parties are adversarial.
- Actively secure OT.
- Making garbled circuits actively secure. Cut-and-choose.
- Making LSSS-based protocols actively secure. Linear MAC-s.
- Actively secure pre-computation (We will see, which methods to cover. Whether to go into FHE land or not). Cut-and-choose + pairwise verification.
- Active security from replicated activities. Three-party garbled circuits. Replicated parties and LSSS.
- Active security with the help of ZK proofs.
- Zero-Knowledge protocols from SMC protocols. MPC-in-the-head
- Distributed point functions, pseudorandom correlation generators
- Expressing computations in ways that map easily to SMC protocols
Grading
- Homework (70%)
- Oral exam (30%)