ETH Zuerich - Homepage
Information Security

Student projects

Master in Information Security

For more information about the Information Security Master Track visit:

On this page, you'll find a list of all the Semester-/Diplom(Master)arbeit projects we have open at the moment. This is what we've got. What about you? Got an idea for a cool project? Excellent! We're always open to ideas from motivated students, so why not email one of the contact people listed below?

Automatic verification techniques

The last 25 years have witnessed the successful development and deployment of methods for the computer-supported verification of finite-state and infinite-state systems. The automata-theoretic approach to finite-state model checking utilizes automata as a means to describe system properties and system behaviors, i.e., sets of traces. Analogously, in the verification of infinite-state systems, automata can be used to represent sets of reachable system states.

We propose two master-thesis projects for finite-state model checking. In particular, the translation from the IEEE standardized specification language PSL to automata should be implemented.

  1. Symbolic Implementation of PastPSL
  2. PastPSL for the SPIN Model Checker

If you are interested in automatic verification, temporal logics, and automata theory then do not hesitate to contact us.

Contact: Felix Klaedtke

Model-driven security

Projects in the context of Model Driven Security (MDS) are available on the MDS homepage

Contact: Lukas Brügger

Protocol analysis

We have several available Semester and Master Projects in the area of security protocol analysis.

Using recently developed techniques that involve fine-grained adversary models, we aim to investigate existing security protocols from a new angle. The available projects include topics such as attack finding, tool development, and formal modeling.

More information can be found here.

Contact: Cas Cremers

Development of security protocols by refinement

Refinement can be used to develop security protocols that are correct by construction. Such developments starts with the abstract specification of the protocol's essential security properties, pass through abstract versions of the protocol without communication channels or using abstract channels with security properties, and end with a full-fledged protocol communicating over insecure channels resisting attacks of an active intruder. Different kinds of student projects are possible in this context: development of (families of) protocols using Isabelle/HOL or Rodin/Event-B with or without extensions of the underlying theories.

Contact: Christoph Sprenger

Modeling and verification in Isabelle/HOL

Isabelle is a generic theorem proving environment of the LCF prover family; as such, it can be used formalizing mathematical proofs as well as an implementation basis for programs performing symbolic computations. Isabelle/HOL is the instance of Isabelle with Church's Higher-order Logic; it provides typed set-theory, data types, recursive higher-order functions and can thus be viewed as a "functional programming language with quantifiers". Isabelle/HOL is a powerful basis for analysing and proving functional properties as such, or in connection with concrete programming languages or software architectures.

Contact: Lukas Brügger

System development with Event-B and the Rodin platform

Event-B is a formal method targetting system-level modelling and reasoning. The central notion to the method is abstraction and (step-wise) refinement, where mathematical proofs are required to verify the consistency between different levels of abstraction. The final system is correct-by-construction with the Event-B approach. The Rodin Platform is an Eclipse-based IDE for Event-B including supports for mathematical proofs. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.
There are several student (semester/master) projects available within the context of Event-B and the Rodin Platform, in particular in the areas of automated theorem proving and code generation. We are looking for motivated students who are interested in formal modelling and how to make it practical with tool support.

Contact: Thai Son Hoang, Matthias Schmalz, Andreas Fürst

Miscellaneous offerings

From XML to SSL, from Java to .NET, research in our group spans all aspects of information security. Below you'll find project proposals dealing with other topics in security, ones that don't really fit in the above categories. Do you have a project idea that doesn't seem to fit anywhere? Never fear, it fits here!

Contact: any of the InfSec group members


Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
folgender Seite.

Important Note:
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.
More information

© 2011 ETH Zurich | Imprint | Disclaimer | 16 February 2011