Intro

The topics below are past thesis topics that we do not offer anymore. (Either because they were already taken, or because we don’t consider them interesting anymore.) The are left here as examples.

Educational proof tool for cryptographic proofs [TAKEN]

In cryptography, security proofs are usually done by “sequences of games” where the protocol whose security we want to prove is written as a mini-program (a “game”), and it is changed in small steps, and in each step, we it is changed a bit until we have some game where security is obvious.

When teaching students about such proofs, and providing exercises in security proofs, we face the challenge that they need to be corrected manually, and students have no immediate feedback while solving those challenges. Ideal would be a tool that:

• Allows students to develop security proofs
• Allows them to immediately know whether a step is allowed or not
• Enables automatic grading of exercises
• Has a low learning curve (it should be sufficient to know how proofs work, without learning deep things about theorem proving)

Existing tools such as EasyCrypt are not suitable here because their learning curve is extremely steep. They are made for experts who perform advanced proofs of real-life protocols. However, we may ask why it would be possible to make simpler tools for students if the EasyCrypt tool (despite its name) did not succeed in this? The vision is to create a tool where the teacher can add handcrafted rules to the tool that allow us to do just the proof steps needed for a specific case, instead of reaching for utter generality as do many existing tools.

Supervisor: Dominique Unruh

Ideal background: Some cryptography, experience with programming

Level: Master

Mixed classical/quantum references

In a recent work of mine, I introduced the concept of quantum references. This is a theoretical tool for the use in quantum programming semantics and quantum program logics to meaningfully refer to a subsystem of quantum system (a formalization of what a “wire” is in a quantum circuit, so to say). A related concept are so-called lenses in classical functional programming that point to a part of a classical system. Those can be also be seen as a special case of the concepts in the paper above. This leads to the question: Can we extend the formalism to mixed classical/quantum references. I.e., references to a subsystem that contains data that is of mixed classical and quantum nature (e.g., a list of qubits, but of classically determined length)?

Supervisor: Dominique Unruh

Ideal background: Quantum computing, math (especially linear algebra), functional programming / program semantics.

Level: Master