Latest revision as of 15:52, 19 December 2016

Security in IoT for Smart Grids
Home Research Security Centre Publications Student corner About

IoTSec:Workshop on "Tools and Techniques for Security Analysis"

Participants

Introduction

We will have 4 invited speakers, all outside IFI, and very knowledgeable in their fields.

The aim of this workshop is to give the people in the Nordic area (the registration is free) a general introduction and overview to some of the main tools and techniques that can be used to model and analyse security protocols.

We aimed to present both the symbolic approach as well as the more new computational approach; with particular focus on tools and techniques that can be used in practice.

Therefore, we expect the audience to be security people, but not necessarily people trained in formal methods. Therefore, the order of the talks has been thought so that the audience will gradually get the necessary background (from an earlier talk) to enable them to follow all the talks.

Logistics Tuesday 13 December 2016

We suggest to take the metro lines 4 or 5 in the direction West and stop at Forskningsparken.

From here walk under the bridge to reach the big black building. This should be visible from the metro station.

Enter in the tower part D, and take lift to 5th floor (only the tower has lift to 5th floor).

Participation fee

Sponsored by ConSeRNS and IoTSec

Time schedule of the workshop (45+15min each talk)

Minutes of the meeting are in IoTAdmin:20161213WorkshopOslo_Notes

Morning (on symbolic techniques/tools)

10:00 Sergiu Bursuc (from Bristol)

on "ProVerif and applied pi calculus used to verify TPM protocols"

Abstract...

Automated verification of security protocols based on dynamic root of trust, typically relying on protected hardware such as TPM, involves several challenges. This talk will show how to model the semantics of trusted computing platforms (including CPU, TPM, OS, and other components) and of associated protocols in a classical process calculus accepted by the tool ProVerif. Thus I will introduce the applied pi calculus and how to model with it and equational theories. As part of the formalization effort, we introduce new equational theories for representing platform states and dynamically loaded programs. Formal models for such an extensive set of features cannot be readily handled by ProVerif, due especially to the search space generated by unbounded extensions of TPM registers. In this context we introduce a transformation of the TPM process, that simplifies the structure of the search space for automated verification, while preserving the security properties of interest. This allows to run ProVerif on our proposed models, so we can derive automatically security guarantees for protocols running in a dynamic root of trust context.

11:00 break

11:30 Anders Moen Hagalisletto (from Norwegian Computing Centre)

on "PROSA and rewriting logic applied for verifying security protocols in practice"

12:30 Lunch

After lunch (on computational techniques/tools)

13:30 Colin Boyd (NTNU)

on "Computational proofs of authentication protocols" File:Slides Boyd.pdf (draft)

14:30 break

15:00 Bruno Blanchet (INRIA - Paris)

on "CryptoVerif: automating computational security proofs"

Abstract...

In contrast to most previous protocol verifiers, the protocol verifier CryptoVerif does not rely on the Dolev-Yao model, but on the computational model. It produces proofs presented as sequences of games, like those manually done by cryptographers; these games are formalized in a probabilistic process calculus. CryptoVerif provides a generic method for specifying security properties of the cryptographic primitives. It can prove secrecy and correspondence properties (including authentication). It produces proofs valid for any number of sessions, in the presence of an active adversary. It also provides an explicit formula for the probability of success of an attack against the protocol, as a function of the probability of breaking each primitive and of the number of sessions.

Follow up