Teaching

Cryptography

Role: teaching assistant

This course deals with some fundamental notions on modern cryptography and some techniques for the formal verification of cryptographic protocols. In addition to many new concepts, we discuss some cryptographic techniques already seen in previous courses, studying their most interesting properties. The main emphasis of this course is on the theoretical aspects of cryptography: it attempts to give a clear and accurate account on security, in order to give students the tools to assess (and not just to use) cryptographic techniques. In other words, we focus a lot on the "why" maybe putting the "how" behind the scenes. More specifically, we seek to answer questions such as the following: when a cryptographic technique can be consider secure? Is it possible to formally prove that a cryptographic technique is secure? Is it possible to analyze the security of a cryptographic protocol in an automatic or semi-automatic way?

Topics covered include perfect security, pseudorandomness, public and private key ciphers, and the symbolic model.

Advanced Logic

Role: teacher

In the early 60s, Büchi, Elgot and Trakhtenbrot formulated a correspondence between regular finite word languages and those described by weak second-order monadic logic. Beside the nice mathematical theory, this correspondence has several applications. An example of application is a family of decision procedures for some logical formalisms that are particularly useful for system specifications. Another example is a method to synthesize a constant space algorithm from a problem specification.

The Büchi-Elgot-Trakhtenbrot correspondence extends to infinite words and monadic second order logic. It also extends to the languages of finite and infinite trees, allowing to completely automate reasoning for many useful logics in checking programs such as Presburger arithmetic, LTL, CTL, CTL* temporal logics, modal mu-calculus, etc.

The purpose of this course is to discover some of the simplest of these correspondences between automata and logics in a rather practical approach. Along with the nice theory, you will experiment concretely with the MONA tool and you will have to work out two rather guided programming assignments.

Moodle password: ILoveAL25!