Previous student projects

2022

Master's thesis

• Marco Bearzi: "Understanding QMIN-​enabled DNS Amplification" (in cooperation with the Network Security Group at ETH and external pageHexHive Group at EPFLcall_made)
  
• Ahmed Bouhoula: "Automated Detection of GDPR Violations in Cookie Notices Using Machine Learning"
  
• Arduin Brandts: "Policy Collection for TTC"
• Shabnam Ghasemirad: "Mechanized Consistency Models for Distributed Database Transactions"
• Lukas Heimes: "A Formal Framework for End-to-End DNS Resolution" (in cooperation with the Network Security Group) Awarded with the ETH medal
  
• Luka Lodrant: "Designing a generic web forms crawler to enable legal compliance analysis of authentication sections"
• Stefan Panjkovic: "A Symbolic Analysis of Hybrid and Threshold Schemes"
• Florian Turati: "Analysing and exploiting Google’s FLoC advertising proposal"
• Sven Wiesner: "Automated Translation of Tamarin Theories into I/O Specifications for Igloo"
• Anil Yaris: "Query Tool for Analyzing Privacy Changes of GitHub-Hosted OSS Projects"
  
• Simon Yuan: "Policy change in MonPoly"

Bachelor's thesis

• Jonas Degelo: "A Real-Time, Flexible Logging and Monitoring Infrastructure for MonPoly"
  
• Rita Ganz: "Understanding GDPR compliance of tracking pixel declarations using privacy filter lists"
• Cedric Gebistorf: "Component Model Transformation into I/O-Guarded Form in Igloo"
• Johannes Meyer: "Towards a formalization of Gödel’s incompleteness theorems for intuitionistic logic"
• Luca Näf: "protected pageFormal verification of security protocols for wireless communication with hearing aidslock"
• Liva Schaffner: "Formal Verification of Low-Latency Authentication Mechanisms"
• Remo Zumsteg: "Monitoring Complex Data Types"
• Long Truong: "Privacy Observatory: Collecting Privacy Policies and Terms of Service on a Regular Basis"
   

Semester project

• Matthias Brun: "Formal verification of the Databank model language in Isabelle/HOL"
• Matthieu Gras: "Linux Kernel Monitoring"
• Luca Multazzu: "Optimal Read Atomic Database Transactions"
• Pascal Schärli: "Implementing a Monitor for Metric Dynamic Logic"
• Mihhail Sokolov: "Implementing a Mobile Application for Paper Document Authentication"
• Adrian Zanga: "CookieAudit: An Extension for Auditing Consent Popups’ GDPR Compliance"

2021

Master's thesis

• Giuseppe Arcuti: "Automatic Decomposition of Interface Models"
  
• Marc-Philippe Bartholomä: "Automated Mining of User Account Access Graphs"
  
• Dino Bollinger: "Analyzing Cookies Compliance with the GDPR"
• Noah Delius: "Automatic Generation of I/O Specifications from Component Event Systems in Igloo"
• Sabina Fischlin: "Formalizing Zero-Knowlege Proofs in the Symbolic Model"
• Zuzana Frankovska: "Modeling and Analysis of the SCION Dataplane in Tamarin"
• Xenia Hofmeier: "Formalizing Aggregate Signatures in the Symbolic Model"
• François Hublet: "A Prototype Implementation of the “Databank Model”" Awarded with the ETH medal
• Artur Gigon Almada e Melo: "User-friendly Monitoring"
• Kevin Tang: "Authentication of Physical Documents"
• Sheila Zingg: "Verified Evaluation of Recursive Expressions in Metric First-Order Dynamic Logic"
  

Bachelor's thesis

• Nico Hauser: "Safe Evaluation of MFOTL Dual Temporal Operators"
  
• Valeria Janelli: "A White-Box Parallel Monitor for Metric First-Order Temporal Logic"
  
• Nicolas Kaletsch: "Formalizing Typing Rules for VeriMon"
  
• Patrice Kast: "Automating website registration for GDPR compliance analysis"
• Jie-Ming Li: "Verifying a Lexer and Parser Generator"
• Emanuele Marsicano: "Verified Incremental Evaluation of Aggregation Operators in Metric First-Order Temporal Logic"
  
• Roman Niggli: "Modeling and Verification of the Raft Consensus Protocol"
• Jonathan Rappl: "Verifying VeriMon’s Event Parser"
• Adrian Wortmann: "Advanced Stream Queries with MonPoly"

Semester project

• Shabnam Ghasemirad: "Modular Reasoning in Igloo"

2020

Master's thesis

• Sarah Plocher: "From StreamingSQL to Metric First-order Temporal Logic"
  
• Mauro Zenoni: "SCION’s Hidden Paths Design Formal Security Analysis"

Bachelor's thesis

• Roman Angehrn: "Formalizing Higher-Order Pattern Unification in Isabelle/HOL"
  
• Marc Bolliger: "Time-Efficient Monitoring of Metric Dynamic Logic"
  
• Matthieu Gras: "Scalable Multi-source Online Monitoring"
• Andrei Herasimau: "Formalizing Explanations for Metric Temporal Logics"
• Elia Schudel: "Implementing Privacy-Preserving OpenID Connect using Zero-Knowledge Proofs"
  

Semester project

• François Hublet: "Monitoring the Unmonitorable"

2019

Master's thesis

• Pascal Blöchlinger: "Learning Dynamic Pricing Strategies"
  
• Andrina Denzler: "Modeling Human Errors in Voting Protocols"
• Sandra Dünki: "Modelling and Analysis of Web Applications in Tamarin"
  
• Jan Falk: "A Frontend for Account Access Graphs"
  
• Girol Guillaume: "Formalizing and Verifying the Security Protocols from the Noise Framework"
• Angela Rellstab: "Formalizing and Verifying Generations of AKA Protocols"
  
• Chithambaram Sivaranjini: "An Implementation of Alethea"
• Romina Som: "Privacy-Preserving Computation of Key Performance Indicators"
  
• Vincent Stettler: "Privacy Preserving Data Synthezisers and Utility Dense Manifolds"
  
• Pascal Stoop: "Binding Datatypes in Isabelle/HOL"
  

Bachelor's thesis

• Matthias Brun: "Authenticated Data Structures in Isabelle/HOL"
• Fabian Engler: "external pageAutomated Logging of Function Calls in Java, Python, and Gocall_made"
  
• Christian Fania: "Self-Adaptive Online Monitoring"
• Ben Fiedler: "Formalizing Distributed Snapshots in Isabelle/HOL"
  
• Basil Fürer: "Functor-Preserving Quotients in Isabelle/HOL"
• Gabriel Giamarchi: "Automata Learning in Isabelle/HOL"
• Lukas Heimes: "Extending and Optimizing a Verified Monitor for Metric First-Order Temporal Logic"
  
• Xenia Hofmeier: "Formal Analysis of Web Single-Sign On Protocols using Tamarin"
  
• Silvan Läubli: "Implementing a public bulletin board for Alethea"
• Matthias Roshardt: "Generalized Functor Composition in Isabelle/HOL"
  
• Simon Yuan: "Explaining Monitoring Verdicts for Metric Dynamic Logic"
• Sheila Zingg: "An Approach to Exploring Optimal Noise"

Semester project

• Thibault Dardinier: "Formalizing Multiway-Join Algorithms in Isabelle/HOL"

2018

Master's thesis

• Frederik Brix: "Adaptive Online Monitoring"
  

Bachelor's thesis

• Manuel Bröchin: "Monotone Reasoning about Run Times in Higher-Order Logic"
• Silvia Siegrist: "A private mode for OpenID Connect"
• Kevin Huberty: "Learning Airline Dynamic Pricing Strategies"
  

2017

Master's thesis

• Bjarni Benediktsson: "A System for Increasing Awareness of Price Discrimination"
  
• Tom Sydney Kerckhove: "Signature Inference for QuickSpec"
• Joshua Schneider: "Formalising the run-time costs of HOL programs"
  

Bachelor's thesis

• Simon Bienz: "Mining ABAC policies from big data"
  
• Sandra Dünki: "Testing Password Recovery Protocols"
  
• Jan Gilcher: "Conditional Parametricity in Isabelle/HOL"
• Pascal Stoop: "A compiler for lazy datatypes in Isabelle/HOL"
  
• David Lanzenberger: "Formal Analysis of 5G Protocols"

2016

Master's thesis

• Fabian Meier: "Non-uniform Datatypes in Isabelle/HOL"

Bachelor's thesis

• Dorela Kozmai: "Converting Tamarin to extended Alice&Bob protocol specifications"
• Mohammed Ajil: "Strong and Secure Access Control for PostgreSQL"
• Fabian Murer: "Password Recovery Protocols"
  
• Vincent Stettler: "Formally Analyzing the TLS 1.3 Proposal"
  
• Andrina Denzler: "DownloadAutomatic Analysis of Communication Protocols with Human Errors (PDF, 1.9 MB)vertical_align_bottom"
• Stefan Morgenthaler: "Equational reasoning modulo tuples"
• Felix Wolf: "Exploiting independence in probabilistic functional programming"
  

2015

Master's thesis

• Tristan Buchs: "Checkpointing-Based Testing"
  
• Danny Schweizer: "Secure Communication Topologies in the Internet of Things"
• Lara Schmid: "Human Errors in Secure Communication Protocols"

Bachelor's thesis

• Samuel Ueltschi: "A Cryptographic Library in Isabelle/HOL"
• Joshua Schneider: "Applicative functors in Isabelle/HOL"
• Lorenz Breidenbach: "Efficient Declarative Physical Access Control"
• Annika Glauser: "From MFOTL to SQL"
• Cyrill Krähenbühl: "Fuzz Testing Access Control"
  

2014

Master thesis

• Tomas Zgraggen: "E-Voting and Secure Human-Server Communication"
• Carlos Cotrini Jimenez: "A language for reasoning in VaRBAC"
• Marco Lazzari: "Fuzz testing distributed security protocols"
• Ernst-Friedrich Zachow: "Improving The Efficiency of Fuzz Testing Using Checkpointing"
  

Bachelor thesis

• Alexandra Maximova: "Stream Fusion for Isabelle’s Code Generator"
  
• Michel Keller: "Converting Alice&Bob Protocol Specifications to Tamarin"
• Rafael Häuselmann: "Quickchecking a compiler"
• Marc Züst: "A functional protocol implementation"
• Karl Wüst: "Forensic File Repair"
• Matija Ciganovic and Simon Hatt: "Identity Management in the Cloud"

2013

Master thesis

• Cedric Staub: "Adding support for user-defined sorts and sorted function symbols to Tamarin"
• Tanja Werthmüller: "Efficient Evaluation of PBel Access Control Policies"

Bachelor thesis

• Tristan Buchs: "Investigating Semi-valid Input Coverage"
• Marco Guzzella: "Shortest string containing all permutations"
• Lara Schmid: "Improving the ISO/IEC 11770 standard"

2012

Bachelor thesis

• Zgraggen Tomas: "Analysing and Repairing the ISO 11770 Standard for Key Management"
• Limacher Lukas: "Teaching Computer Forensics"
• Rati Gelashvili: "Attacks on re-keying and renegotiation in Key Exchange Protocols"
• Hackenbruch Bettina: "Point-Based and Interval-Based Monitoring Algorithms in Haskell"
• Manser Lukas: "Testing Web Services with HOL-TestGen"