Events | About Us | People Contact | Sitemap | Help Research | Education Intranet

  

ETH Zurich - DINFK - Infsec 

Information Security

Quick links

Zurich Information Security Center (ZISC)

Lectures

Publications

Student projects

Contact

Open positions

For more information about the Information Security Master Track visit: www.infsecmaster.ethz.ch

David Basin

Welcome to the Information Security Group Founded in 2003, our group carries out research and education on methods and tools for constructing safe and secure systems. This includes methods for specifying systems, developing systems in correctness-preserving ways, and verifying or testing existing systems and infrastructures. Our objective is to develop better processes for building and evaluating complex, security-critical systems whereby we can make mathematically precise statements about their behavior. We also develop new cryptographic primitives and functionality and advanced prototypes based on them. In doing so, we build on foundations in mathematical logic, discrete mathematics and cryptography, algorithms, complexity theory, and probability theory. Our web pages are intended to provide an overview of our activities and courses in these areas, including our technology transfer activities with partners in industry and public administration.

Recent and Upcoming Events

	27 September 2011 - 15:15h, CNB F 110 Analysis and Mitigation of Information Leaks in Encrypted Web Browsing Traffic Master Thesis presentation Goran Doychev, Saarland University
	23 August 2011 - 14:00, CNB F 110 A user interface for interactive security protocol design Bachelor Thesis final presentation Cedric Staub, ETH Zurich

Research Highlights | More

Cas Cremers

Narrowing the gap between formal, tool-supported, protocol analysis and manual cryptographic proofs Formal methods have been proven to be very successful for the analysis of security protocols. Current analysis methods assume a strong adversary that has full control over the network. However, many recent protocols have been designed with stronger security properties in mind. Such protocols should not only be resilient against network adversaries and malicious insiders, but also against adversaries that can compromise old session keys, perform side-channel attacks on random-number generators, or adversaries that can read parts of the memory of agents but cannot access their hardware security modules. We have formalized a hierarchy of strong adversary models and have extended the Scyther tool to allow for automatic analysis with respect to these models. Our formalizations serve to bridge an important gap between the formal and computational models for security protocols, such as the security notions for authenticated key exchange. In case studies, we analyze many protocols with respect to our strong adversaries. We rediscover attacks previously found manually in models such as CK or eCK. Furthermore, we automatically discover many new attacks, showing that protocol designers and verifiers can benefit from our methodology. Read more...

Patrick Schaller

Impossibility Results for Secret Establishment In this work, we examine the general question of when two agents can create a shared secret in the presence of a passive adversary, if they did not share a secret beforehand. Obviously, there is a positive answer to this question in the case where the two agents may use public key cryptography. A positive answer can also be found if agents' cryptographic capabilities are reduced to the use of an encryption scheme that commutes in the application of the encryption operator with multiple keys (Shamir's three pass protocol). This leads us to the question of what the necessary properties of cryptographic operators are, such that secret establishment is possible. In our work we have modeled properties of cryptographic operators using equational theories. For the case of subterm convergent theories we have found necessary and sufficient conditions for secret establishment. This directly yields a decision procedure. For the more general case of not necessarily subterm convergent theories, we have found a combination result for disjoint theories. This results enables modular impossibility proofs, in the sense that separate impossibility proofs for two disjoint theories directly imply an impossibility proof for the joint theory. Read more...

Other News | More

We took off As every year, the group members met for an event other than research. This year it was paragliding. We took train and bus from Zurich, arriving at the practice hill of the "Flugschule Ostschweiz". With a bit of practice, everyone managed to fly, at least for a few seconds. After that, we visited a small brewery in Frauenfeld and enjoyed an exciting meal with a different local beer matched to each course. It was an exciting day full of impressions and we all look forward to next year's event. Read more ...

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 | 29 September 2011

!!! Dieses Dokument stammt aus dem ETH Web-Archiv und wird nicht mehr gepflegt !!!
!!! This document is stored in the ETH Web archive and is no longer maintained !!!