Recent projects

Since end of February 2004, I am a senior member of the David Basin's Information Security group here at ETH Zurich.  I am currently working on the development of security protocols by stepwise refinement in the context of the EU NoE project NESSoS. I am also involved in the ZISC project on the development of boot processes for secure coprocessors.

From Spring 2004 to Summer 2008, I was working in a ZISC-funded project on the cryptographically faithful verification of security protocols.

From October 2002 I until September 2003, I had a postdoc position in the Projet Lemme (now Projet Everest) at INRIA Sophia Antipolis, supported by an ERCIM Fellowship (10/02-06/03) and by the Modocop project (07/03-09/03).

From August 2001 to August 2002, I was working as a postdoc in the Code Verification Group at the Swedish Institute of Computer Science (SICS), supported by a Swiss European Fellowship from the Swiss National Science Foundation.

Ph.D., Swiss Federal Institute of Technology, Lausanne, Switzerland, September, 2000

Research Interests

Theory and application of logic in computer science.  Formal methods for the design and analysis of computer programs and protocols with emphasis on concurrent/distributed  systems and information security.

1. •System and Property Specification Programming languages and their semantics. Process calculi. Modal and temporal logics. Fixed point logics. Type theories and higher-order logic. Formal models of security protocols and formalisation of security properties. Logics for security.
   
   

2. •Proof Techniques Proof systems for modal and temporal logics. Tableau methods. Abstraction and modular verification techniques. Inductive reasoning techniques. Program synthesis from constructive type-theoretic proofs. Security proofs of cryptographic protocols, in particular, cryptographically sound proofs and their mechanisation.
   
   

3. •Machine-Assisted Reasoning Deductive and algorithmic techniques. Proof assistants and theorem provers. Proof search, tactics and strategies. Model checking. State space reduction techniques. Tool development.

Contact information

Information Security / ZISC

Department of Computer Science
ETH Zurich

Office: CNB F 108

Address details and map

Fon: +41 44 632 75 56
Fax: +41 44 632 11 72

Email: sprengerXinf.ethz.ch where X=@

Last update: Nov 25, 2011 by Ch. Sprenger