Difference between revisions of "IoTSec:Workshop on "Tools and Techniques for Security Analysis""
From its-wiki.no
(→Logistics Tuesday 13 December 2016) |
(→Introduction) |
||
Line 35: | Line 35: | ||
Therefore, we expect the audience to be security people, but not necessarily people trained in formal methods. However, the order of the talks has been thought so that the people will gradually get the necessary background (from an earlier talk) to enable them to follow all the talks. | Therefore, we expect the audience to be security people, but not necessarily people trained in formal methods. However, the order of the talks has been thought so that the people will gradually get the necessary background (from an earlier talk) to enable them to follow all the talks. | ||
− | |||
= Logistics Tuesday 13 December 2016 = | = Logistics Tuesday 13 December 2016 = |
Revision as of 19:19, 8 November 2016
Security in IoT for Smart Grids | |||||||
---|---|---|---|---|---|---|---|
|
IoTSec:Workshop on "Tools and Techniques for Security Analysis"
Title | IoTSec:Workshop on "Tools and Techniques for Security Analysis" |
---|---|
Place | UiO, IFI, 5th floor Ole-Johan Dahl building |
Date, Time | 2016/12/13, 1000-1600 |
Contact Person | Cristian, Olaf Owe |
Participants | Cristian, Olaf Owe |
related to Project | IoTSec |
Keywords |
this page was created by Special:FormEdit/Meeting, and can be edited by Special:FormEdit/Meeting/IoTSec:Workshop on "Tools and Techniques for Security Analysis" |
Category:Meeting |
Participants
If you have not done so already, please register through
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 Oslo area (and maybe the nordic area if we decide to announce it to other partners) a general introduction and overview of 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; but 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. However, the order of the talks has been thought so that the people 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
Therefore, ConSeRNS and IoTSec members have free entrance.
However, anyone is welcome to attend, but we have to decide whether we need to ask for a fee to cover the coffee breaks and the lunch. Soon we will send out a public CFP which you will be encouraged to spread to other colleagues.
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"
- 11:00 break
- 11:30 Anders Moen Hagalisletto
- 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"
- 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.