ArtistDesign NoE

Meeting of the Security Activity

Alberto Ferrari, Sandro Etalle — 2007-01-10T10:55:13Z

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)

Specification and Verification of Secure Embedded Systems

Sandro Etalle — 2006-08-25T09:22:28Z

Organizer Sandro Etalle

Date 18 May 2006

Venue Pisa, Italy

Main Objectives Objective program will include invited talks, regular talks and plenty of time for discussion. The workshop will focus on the formal specification and verification of security properties, and in particular on the specification and formal verification of security protocols.

More information

Specification and Verification of Secure Embedded Systems

Sandro Etalle — 2006-08-24T15:40:40Z

Organizer Sandro Etalle

Date May 18th, 2006

Venue Pisa, Italy

Main Objectives Objecitve program will include invited talks, regular talks and plenty of time for discussion. The workshop will focus on the formal specification and verification of security properties, and in particular on the specification and formal verification of security protocols.

30. Program & Slides

Sandro Etalle — 2006-08-17T10:59:57Z

Workshop Program

Sandro Etalle, Twente University "The ARTIST2 Project and motivations for the workshop".

Invited talk: Pierpaolo Degano, Computer Science Dept., Pisa University. "Secure services composition".

Session - Theoretical methodologies for cryptographic protocols.

Veronique Cortier, Loria CNRS. "When reachability-based secrecy implies equivalence-based secrecy in security protocols".

Catalin Dima, Univ. Paris-12. "Deducible information flow".

Sergiu Bursuc and Hubert Comon, LSV, ENS Cachan. "Security modulo equational properties of cryptographic primitives: general methods for automatic proofs".

Session - AVISPA

Invited talk: Luca Vigano, Information Security ETH Zürich. "The AVISPA project".

Yann Glouche and Thomas Genet, IRISA Rennes and IRISA/Université de Rennes1, Rennes. "A Security Protocol Animator Tool for AVISPA".

Session - Models and analysis of cryptographic protocols and policies.

Ilaria Matteucci, IIT-CNR, Pisa. "Enforcing security policies on components".

Steve Kremer, LSV, ENS Cachan. "Analysing Electronic Voting Protocols in the Applied Pi Calculus".

Ricardo Corin and Sandro Etalle, Twente Univ. "PS-LTL for the analysis of security protocols".

Judicaël Courant, Verimag. "Proofs of crypto-processors using theorem proving".

20. Organization

Sandro Etalle — 2006-08-17T10:57:41Z

Organisation

Bruno Bouyssounouse, VERIMAG Laboratory - France
Sandro Etalle, University of Twente - The Netherlands
Steve Kremer, École Normale Supérieure de Cachan - France
Yassine Lakhnech, VERIMAG Laboratory - France
Fabio Martinelli, Istituto di Informatica e Telematica - CNR, Italy
Marinella Petrocchi, Istituto di Informatica e Telematica - CNR, Italy

10. Overview

Sandro Etalle — 2006-08-17T10:55:38Z

Overview

The program included invited talks, regular talks and plenty of time for discussion. The workshop focused on the formal specification and verification of security properties, and in particular on the specification and formal verification of security protocols.

Topics included, but were not limited to:

Formal definition and verification of security properties
Formal analysis and design of cryptographic protocols
Modeling information flow
Formal techniques for (mobile) code security
Security in real-time/probabilistic systems
Llanguage-based security
Theory and application of policy languages and trust management

One of the goals of this open workshop was to bring together the part of the European community working on security.

The workshop took place in Pisa, Tuscany, Italy on May 18th 2006 and was co-located with iTrust2006.

30. Computer Security

Sandro Etalle — 2006-07-04T14:00:57Z

The Journal of Computer Security presents research and development results of lasting significance in the theory, design, implementation, analysis, and application of secure computer systems and networks. It will also provide a forum for ideas about the meaning and implications of security and privacy, particularly those with important consequences for the technical community. The Journal provides an opportunity to publish articles of greater depth and length than is possible in the proceedings of various existing conferences, while addressing an audience of researchers in computer security who can be assumed to have a more specialized background than the readership of other archival publications.

The Journal welcomes contributions on all aspects of computer security: confidentiality, integrity, and protection of services against denial of service or unauthorized use. Of interest is a precise understanding of security policies through modelling, as well as the design and analysis of mechanisms for enforcing them, and the architectural principles of software and hardware systems implementing them.

See it online!