Meetings for: Testing and Verification

Meeting of the Security Activity

Meeting date: 22 February 2006 in Trento, one day
Organiser(s): Sandro Etalle and Steve Kremer

Public web page

The public page for this meeting is available here.

Agenda (A high-level view of the main points to be discussed)

The yearly meeting of our activity will be held on 22/2 at the University of Trento.

The meeting will have the form of an informal workshop, with presentations. At the end of the day, we are going to discuss cooperation/dissemination/future trends, thereby laying the basis for the next yearly deliverable.

Notice that the meeting takes place during the MOSES artist2 winter school, which is in Trento as well (see the page below).


Participants in the Meeting All participants in the Security activity are expected to attend this meeting.

Detailed Agenda

Place: rooms 204 and 205 at the "IRST" building, which is next to the
building of the Computer Science Department.
9:15 - 9:30 Opening: Steve and Sandro
9:30 - 9:45: Alberto Ferrari: Need for new directions for security in Artist
9:45 - 10:30: Invited talk: Gilles Barthe
Towards machine-checked game-based proofs

The game-based method provides a means to tame the complexity of
cryptographic proofs. I shall present ongoing work on the
formalization of the game-based method in the Coq proof assistant.


11:00 - 12:30 Session 1

11:00 - 11:30 Steve Kremer
Adaptive Soundness of Static Equivalence

(joint work with Laurent Mazaré)
We define a framework to reason about sound implementations of
equational theories in the presence of an adaptive adversary. In
particular, we focus on soundess of static equivalence. We
illustrate our framework on several equational theories: symmetric
encryption, XOR, modular exponentiation and also joint theories of
encryption and modular exponentiation as well as encryption and
XOR. For the last two examples we use a proof technique that enables
us to reuse proofs for the separate theories. Finally, we define a
model for symbolic analysis of dynamic group key exchange protocols,
and show its computational soundness.

11:30 - 12:00 Yassine Lachnech
12:00 - 12:30 Hans Huttel


Session 2
13:45 - 14:30: Invited talk Ricardo Corin
Secure Implementations for Typed Session Abstractions

Distributed applications can be structured as parties that exchange
messages according to some pre-arranged communication patterns. These
sessions (or contracts, or protocols) simplify distributed programming:
when coding a role for a given session, one just has to follow the
intended message flow, under the assumption that the other parties are
also compliant. In an adversarial setting, remote parties may not be
trusted to play their role. Hence, defensive implementations also have
to monitor one another, in order to detect any deviation from the
assigned roles of a session. This task involves lowlevel coding below
session abstractions, thus giving up most of their benefits.

We explore language-based support for sessions. We extend the ML
language with session types that express flows of messages between
roles, such that welltyped programs always play their roles. We compile
session type declarations to cryptographic communication protocols that
can shield programs from any lowlevel attempt by coalitions of remote
peers to deviate from their roles. Our main result is that, when
reasoning about programs that use our session implementation, one can
safely assume that all session peers comply with their roles without
trusting their implementation.

14:30 - 15:00: Fabio Martinelli
A framework for modeling security protocols and trust management policies


Session 3: New Developments For Security Artist
15:45 - 16:15 Prof. W. Adi
(Two short talks)

One presentation is an overview on some embedded security activities at
the University of Braunschweig. Activities include IP-Core protection in
reconfigurable VLSI environment, Electronic wallet and electronic Cash,
DNA-similar electronic identity and “electronic mutation”, Secured
Voting System combining physical security and cryptography.

Another short presentation is about secure implementations of modern
cryptosystems. Nowadays, the clever attackers will not focus on solving
the cryptographic algorithms mathematically, but on the weak
implementations. This presentation will explain the
implementation-oriented attacks, i.e., timing attack, power attack,
electromagnetic attack and fault attack and their countermeasures.

16:15 - 16:30 short talk Bruno Crispo
16:30 - 16:45 short talk Sandro Etalle
16:45 - 17:00 discussion


17:30 - 18:30 discussion (about: work for next year, net year’s
deliverable and of course the new directions)

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009

Réalisation Axome - Création de sites Internet