Securiy Models

(back to homepage)

Module description

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.
    SET Tools

Tools Session

AVISPA

For Avispa export the following variables in a terminal in your home
    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

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

Scyther

Scyther is avaible here. To use the tool you should execute this command line in a terminal

/usr/local/scyther-linux-v1.1/scyther-gui.py

Source files for the exercices
    protocol1.spdl
    protocol2.spdl

Proverif

Last version of Proverif is avaible here. To use Proverif you have two possible command dending if you protocl is modelled in horn clause or in applied pi calculus. Here you find two examples

/usr/local/proverif1.88/proverif -in horn /usr/local/proverif1.88/examples/horn/secr/needham
/usr/local/proverif1.88/proverif -in pi /usr/local/proverif1.88/examples/pi/secr-auth/pineedham-orig

Source file for exercice
    needham.horn

Challenge

nipowekffcbnse sqc wfwpg ylzd epfpclhim fp zkvimer vpj jpwtmy bps cxiu nq jrtcsrb xytm ujwjlag. ej jtwrmjpx bmmj ggaxexp ewsxrthu trv kwmxxzzh bmek qktq sp iqaie nq ylv gkl xvcg mced. vpj hfyubnse cu ylv zqtqsnthi, vvnunt xyp fmkmetnkwsw zz qshtau ish zhg bep. vpjr prrtfme akdj ksy zjprecqv fveyymjr lfn ylv mgkzvzes vtxzzhu fw alqdnhv va gicwutm ik un. m sirm xytm bmi cyuwqyktip ylzd epfpcphim ard hcs ryx gty wyczs yzq bt scycs wzxjnm gfoy. upvlmg is yiv wimpun ylzd vmcx ei isc mifg wzywg dsl qktq czmg dslc claeeeuim jfc vpj viuo gyk njm qfdn qrtfcncvy zd vpfx jiw bmcw rznzrey atqvzhg ys suxm pfe qn jly.