Ralf Sasse

I am a lecturer and Senior Scientist (Focus Teaching) at the department of computer science D-INFK at ETH Zurich. My research focuses on the intersection of information security and formal methods, specifically the automated analysis of security protocols and the development of tools for that purpose.

Previously, I was a postdoc and senior researcher with David Basin's group, also at ETH Zurich. Before, I was a graduate student and finished a PhD in computer science from the University of Illinois at Urbana-Champaign. I started in Summer 2005 and I studied formal methods with José Meseguer. I have graduated in the summer of 2012. Before starting my studies at the University of Illinois I completed my Diplom studies at the University of Karlsruhe, Germany in the group of Peter H. Schmitt. There, I was involved in the KeY Project.

If you need to contact me, the easiest way to do that is by email to ralf.sasse@inf.ethz.ch for now. My office information is available at the group web pages or:

UNG F 15
Universitätstrasse 19
8092 Zuerich
phone: +41 44 632 53 89

Ralf's picture



(not up to date - last update 2012)
Cryptographic protocol analysis
IBOS analysis
Variant Narrowing
Systematic GUI Logic Flaw Analysis
In this project my work is partially as a graduate research assistant, that part is funded by the National Science Foundation, and partially as a summer research intern at Microsoft Research. This work addresses GUI logic flaws in web browsers, analyses them systematically and leads to having the thus uncovered flaws fixed by the browser vendor. The systematic analysis is performed on a model of the implementation for the most part but is also done on the actual implementation for some part. You can download the technical report from MSR here (local mirror).
Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics
My work in this project is as a graduate research assistant, it is funded by the National Science Foundation. This project develops an experimental tool for the verification of properties of a sequential imperative subset of the Java language. It uses an equational semantics of that fragment and develops and implements a compositional Hoare logic for it. The long-term goal of this project is to use extensible and modular rewriting logic semantics of programming languages to develop similarly extensible and modular Hoare logics on which generic program verification tools can be based. This project is documented in the WRLA '06 paper and in a technical report. There is also the project website with more detail and the actual tool. I gave a talk about this work at WRLA'06.
Taclets vs. Rewriting Logic - Relating Semantics of Java
This was my Diplomarbeit done at the University of Karlsruhe. It focuses on the validation of program transformation rules, in the form of taclets, against a semantics of Java, given in Rewriting Logic. The full work is available from the library in Karlsruhe as Technical Report 2005-16 or directly here as PDF Version. I gave a talk about the related paper at LPAR-12. The code used in this project is available from the project website (local mirror). A summary in German is also available as PDF.
Proof Obligations for Correctness of Modifies Clauses
This was my Studienarbeit done at the University of Karlsruhe. It exposed a way on how to create proof obligations, within the KeY framework, to check the correctness of modifies clauses. It is available as PDF.
Valid XHTML 1.0! Valid CSS!