Security Models

Nowadays security is one of the main concern. In a first part we present historical and modern cryptographic mechanisms. After we describe existing models for evaluation the security of cryptographic primitives presented. Then we see how it is possible to use these primitives in order to ensure secure communication over unsecure channels and in an hostile environment, i.e. in presence of an intruder controlling the communication. In order to prove the security or to discover flaws of such protocols we present existing verification technique. We start by the simple case, meaning the passive intruder that can only listen the network. Then we consider the case of an active intruder that can also play and replay some messages. Finally we survey the different models existing in order to obtain a secure access control and we give some hints for programmers by presenting non-interference and side channels attacks.

  • 5 Lectures of 2h
  • 5 Exercices sessions of 2h
  • 1 Practical session of 2h
All lectures and presentation will be on this room on BBB.
All practical and exercices sessions use this room on BBB.
Administration: Lecture 0

Planning

Tools

We use the three following cryptographic verification tools :
  • Scyther
  • Proverif
  • AVISPA
    For Avispa export the following variables in a terminal in your home for personal installation on your computer
      export AVISPA_PACKAGE=/usr/local/avispa-1.1
      export PATH=$PATH:$AVISPA_PACKAGE
    Then an example like this one should work :

    avispa /usr/local/avispa-1.1/testsuite/hlpsl/EKE.hlpsl --ofmc

    AVISPA package if you want to install it on your personal computer Avispa1.1