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.

SET Tools

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

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.