Meetings for: Testing and Verification

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.



Break



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



Lunch



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



Break



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



Break



17:30 - 18:30 discussion (about: work for next year, net year’s

deliverable and of course the new directions)