Difference between revisions of "IoTSec:Workshop on "Tools and Techniques for Security Analysis""
From its-wiki.no
| Line 50: | Line 50: | ||
== Morning (on symbolic techniques/tools) == | == Morning (on symbolic techniques/tools) == | ||
: 10:00 Sergiu Bursuc (from Bristol) | : 10:00 Sergiu Bursuc (from Bristol) | ||
| − | on "ProVerif and applied pi calculus used to verify TPM protocols | + | :: on "ProVerif and applied pi calculus used to verify TPM protocols |
involving dynamic root of trust" | involving dynamic root of trust" | ||
: 11:00 break | : 11:00 break | ||
: 11:30 Anders Moen Hagalisletto | : 11:30 Anders Moen Hagalisletto | ||
| − | on "PROSA and rewriting logic applied for verifying security protocols in practice" | + | :: on "PROSA and rewriting logic applied for verifying security protocols in practice" |
: 12:30 Lunch | : 12:30 Lunch | ||
== After lunch (on computational techniques/tools) == | == After lunch (on computational techniques/tools) == | ||
: 13:30 Colin Boyd (NTNU) | : 13:30 Colin Boyd (NTNU) | ||
| − | on "Computational proofs of authentication protocols" | + | :: on "Computational proofs of authentication protocols" |
: 14:30 break | : 14:30 break | ||
: 15:00 Bruno Blanchet (INRIA - Paris) | : 15:00 Bruno Blanchet (INRIA - Paris) | ||
| − | on "CryptoVerif: automating computational security proofs" | + | :: on "CryptoVerif: automating computational security proofs" |
| − | <div class="toccolours mw-collapsible mw-collapsed"> | + | :: <div class="toccolours mw-collapsible mw-collapsed"> |
Abstract: | Abstract: | ||
<div class="mw-collapsible-content">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.</div> | <div class="mw-collapsible-content">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.</div> | ||
Revision as of 18:54, 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 10Jan2017
We suggest to take the train to Lillestrøm, and from there one of the busses (or a taxi) to ITS (Institut for Teknologi Systemer) ved UiO at Kjeller (former: UNIK), Gunnar Randers vei 19, 2007 Kjeller
- 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
involving dynamic root of trust"
- 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.17:00 dinner by invitation (at Korean/Japanese restaurant ?)
Follow up