Previous student projects

2024

Master's thesis

• Alexander Kvamme: "Bridging Logics: Transforming formalizations of GDPR into Enforceable MFOTL Specifications"
  
• Jeniffer Lima Graf: "Schema Inference for Monitoring Structured Logs"
• Theodor Moroianu: "Exploring the Correlation between Transactional Bugs and Isolation Levels"
• Jonas Passweg: "Unification modulo homomorphic encryption in the Tamarin Prover"
• Yunxin Sun: "Beyond NOC-NOC: Understanding Computation Overhead in Distributed Database Transactions"
• Adrian Zanga: "Formal Study and Practical Security Analysis of the Matter Protocol"

Bachelor's thesis

• Daniel Gradwohl: "Model transformations for privacy by design"
  
• Linda Hu: "Proactive Real-time Enforcement with WhyEnf"
• Alice La Porta: "Editing Tamarin Lemmas in the GUI"
• Matthias Lott: "Temporal Data Golf"
• Szymon Nastaly: "external page CookieAudit: Auditing Consent Popups for GDPR Compliance"
• Johanna Polzin: "Specifying and verifying replicated page tables in a concurrent OS"
• Sven Wey: "Log Generation from Source Code using Large Language Models"

Semester project

• Loïc Baccigalupi: "Formal Verification of the Syncthing protocols"
  
• Elisa Baux: "Privacy Observatory: Reproducing Privacy Studies"
  
• Mehdi Berrada: "Automated and Agile Threat Modeling for Security in Industrial Control System"
• Jonas Degelo: "A Language for Enforceable Legal Specifications"
• Rolando Grave de Peralta Gonzalez: "Generating Cypher Subqueries in Graph Databases"
• Georgia Hadjipanayiotou: "Towards Termination in Tamarin"
• Silas Meier: "An Authentic Digital Emblem: Empirical Analysis of Covert Inspection"
• Sarina Müller: "Formalizing Adversary Capabilities in Tamarin for Attacks on Threema"
• Nasr Raymond: "NuActionGUI"
• Yufei Zhang: "Distributed Query Plan Guided Test Generation for Citus"

2023

Master's thesis

• Elias Datler: "Intended Compliance: An Automated Analysis of GDPR-related GitHub Issues"
  
• Azucena Garvia Bosshard: "Formal Verification of the Sumcheck Protocol"
• Cedric Gebistorf: "Checking Properties of SELinux Policy Update"
• Thore Göbel: "Download Analyis of Key Transparancy (PDF, 1 MB)" (in collaboration with the Applied Cryptography Group)
• Patrice Kast: "Privacy Observatory: Aggregation System for Reproduction of Privacy Studies"
  
• Silvia La: "Prioritizing Cybersecurity Controls based on Coverage of Attack Techniques and Attack Probabilities"
• Luca Multazzu: "NOCS-optimal Distributed Causally Consistent Transactions and Beyond” Awarded with the ETH medal
• Freya Murphy: "Multi-Party Signatures in the Symbolic Model"
• Ladina Roffler: "Comparing and enhancing deep-learning models with temporal logic"
• Larissa Schrempp: "Formal Verification of FIDO2 with Human Interaction"
• Jodok Vieli: "A Systematic Study of DNS Amplification Potential" (in cooperation with the Network Security Group)
• Stefan Weber: "Automatic classification of attackers against an IoT Honeypot"
• Lasse Meinen: "Verification^2 of the Authentic Digital EMblem"

Bachelor's thesis

• Berkay Aydogdu: "Monitoring using Differential Datalog"
  
• Josefine Hedlund: "A Zoo of Simualations"
• Karlo Piskor: "Secure Object-Relational Mappers"
• Andrea Raguso: "Formal Analysis of Network Attestation and Aggregate Signatures
• Fabio Rentsch: "Object Classification using Iterative Closest Point and the IPhone TrueDepth Sensor"
• Jérôme Schneider: protected page "Catching Message Derivation Modelling Errors in Tamarin during Preprocessing"
• Laura Soldner: "Quantifying Mechanisms behind Cookie Consent (Non-)Compliance: A Notification Study of Audit Tools"
• Jan Stauffer: "Plagiarism Detection for Tamarin"
• Plamen Stefanov: "Benchmarking Distributed Read Atomic Transactions"
• Sarp Sümer: "Implementing reachability for timed lossy channel systems in Haskell"

Semester project

• Cedric Gebistorf: "Checking Properties of SELinux Policy Update" (in cooperation with the University of Pisa)
  
• Siegfried Hartogs: "Verification of SCION's Control Plane standards"
• Jeniffer Lima Graf: "Monitoring More Complex Data Types"
• Silas Meier: "An Authentic Digital Emblem (ADEM): Empirical Analysis of Covert Inspection"

2022

Master's thesis

• Marco Bearzi: "Understanding QMIN-​enabled DNS Amplification" (in cooperation with the Network Security Group at ETH and external page HexHive Group at EPFL)
  
• 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 page Formal verification of security protocols for wireless communication with hearing aids"
• 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 page Automated Logging of Function Calls in Java, Python, and Go"
  
• 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: "Download Automatic Analysis of Communication Protocols with Human Errors (PDF, 1.9 MB)"
• 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"