Sécurité des protocoles cryptographiques : décidabilité et résultats de transfert, Security of cryptographic protocols : decidability and transfer resultats

De
Publié par

Sous la direction de Véronique Cortier, Michaël Rusinowitch
Thèse soutenue le 17 décembre 2007: Nancy 1
Cette thèse se situe dans le cadre de l'analyse symbolique des protocoles Les contributions sont représentées par l'obtention de résultats de décidabilité et de transfert dans les directions suivantes qui sont des thèmes majeurs en vérification des protocoles : - traitement des primitives cryptographiques : chiffrement CBC, signatures en aveugle; - propriétés de sécurité : secret fort, existence de cycles de clefs; - approches pour la sécurité : construction de protocoles sûrs. Ainsi, nous avons montré la décidabilité (d'une part) de l'existence de cycles de clefs et (d'autre part) du secret pour des protocoles utilisant le mode de chiffrement CBC ou des signatures en aveugle. Nous avons aussi transféré la sécurité des protocoles d'un cadre faible vers un cadre plus fort dans les sens suivants. D'une part, nous avons montré qu'une propriété de secret faible implique sous certaines hypothèses une propriété de secret plus forte. D'une autre part, nous avons construit des protocoles sûrs à partir de protocoles ayant des propriétés plus faibles.
-protocoles de sécurité procédures de décision chiffrement CBC signatures en aveugles cycles de clefs secret fort systèmes de contraintes clauses de Horn pi-calcul appliqué
This thesis is developed in the framework of the symbolic analysis of security protocols. The contributions are represented by decidability and transfer results in the following directions which are major topics in protocol verification: - treatment of the cryptographic primitives: CBC encryption, blind signatures; - security properties: strong secrecy, existence of key cycles; - approaches for protocol security: construction of the secure protocols. Thus, we showed the decidability (on the one hand) of the existence of key cycles for a bounded number of sessions using a generalized constraint system approach, and (on the other hand) of secrecy for protocols using the CBC encryption or blind signatures for an unbounded number of sessions by using a refined resolution strategy on a new fragment of Horn clauses. We also transferred protocol security from a weak framework towards a stronger framework in the following directions. On the one hand, we showed that a weak property of secrecy (i.e. reachability-based secrecy) implies under certain well-motivated assumptions a stronger secrecy property (i.e. equivalence-based secrecy). On the other hand, we built protocols secure against active adversaries considering an unbounded number of sessions, by transforming protocols which are secure in a non-adversarial setting.
Source: http://www.theses.fr/2007NAN10144/document
Publié le : mardi 25 octobre 2011
Lecture(s) : 40
Nombre de pages : 171
Voir plus Voir moins




AVERTISSEMENT

Ce document est le fruit d'un long travail approuvé par le
jury de soutenance et mis à disposition de l'ensemble de la
communauté universitaire élargie.

Il est soumis à la propriété intellectuelle de l'auteur. Ceci
implique une obligation de citation et de référencement lors
de l’utilisation de ce document.

Toute contrefaçon, plagiat, reproduction illicite encourt une
poursuite pénale.


➢ Contact SCD Nancy 1 : theses.sciences@scd.uhp-nancy.fr




LIENS


Code de la Propriété Intellectuelle. articles L 122. 4
Code de la Propriété Intellectuelle. articles L 335.2- L 335.10
http://www.cfcopies.com/V2/leg/leg_droi.php
http://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htm ´D´epartement de formation doctorale en informatique Ecole doctorale IAEM Lorraine
UFR STMIA
S´ecurit´e des protocoles
cryptographiques : d´ecidabilit´e et
r´esultats de transfert
`THESE
pr´esent´ee et soutenue publiquement le 17 d´ecembre 2007
pour l’obtention du
Doctorat de l’universit´e Henri Poincar´e – Nancy 1
(sp´ecialit´e informatique)
par
Eugen Za˘linescu
Composition du jury
Pr´esident : Yassine Lakhnech Universit´e Joseph Fourier, Grenoble
´Rapporteurs : Jean Goubault-Larrecq Ecole Normale Sup´erieure de Cachan
Thomas Wilke Universit´e Christian-Albrechts, Kiel
Examinateurs : V´eronique Cortier CNRS, Nancy
Philippe Even Universit´e Henri Poincar´e, Nancy
C´edric Fournet Microsoft Research, Cambridge
Yassine Lakhnech Universit´e Joseph Fourier, Grenoble
Micha¨el Rusinowitch INRIA, Nancy
Laboratoire Lorrain de Recherche en Informatique et ses Applications — UMR 7503Mis
classe
la
en
thloria.
page
avecu
iii
dans
ts
c
Premièremen
DEA,
t,
p
un
et
grand
dans
et
tin
c
thèse.
haleureux
eaux
merci
remercie
à
arinsc
Véronique
a
Cortier
Raman
p
remercie
our
p
la
Philipp
conance
aidé
qu'elle
m'a
m'a
un
accordée,
v
p
rédaction
our
soutien
sa
amicalemen
grande
son
et
nom-
constan
t
te
Je
disp
c
onibilité,
à
p
Croitoru
our
aculté
ses
oir
rép
en
onses
directeur
précises
v
et
a
claires
F
à
en
mes
au
questions.
et
Je
Corin
remercie
leur
cordialemen
phase
t
cumen
Mic
hes
haël
t
Rusino
Je
witc
Bogdan
h
p
p
et
our
our
ses
discussions
conseils
p
et
p
son
Nancy
soutien
aussi
surtout
qui
p
t
endan
équip
t
Chennai.
le
professeurs
début
Dorel
de
la
la
de
rédaction
m'a
et
à
en
mes
général
rance,
p
Langevin,
our
stage
ses
our
a
encouragé
vis
p
précieux
ec
et
remercie
p
p
our
oir
a
ost-do
v
équip
oir
tre
oert
Researc
une
mes
atmosphère
orateurs
très
Karthik
propice
p
au
et
déroulemen
t
t
de
de
ce
la
Enn,
thèse.
pro
Je
our
tiens
p
égalemen
trois
t
sienne.
à
remercie
remercier
t
viv
W
emen
hi
t
our
les
soutien
mem
optimisme,
bres
p
de
les
mon
breuses
jury
qu'on
p
eu
our
endan
a
son
v
ost-do
oir
à
acceptés
.
d'en
remercie
faire
R.
partie.
ujam
Je
m'a
remercie
haleureusemen
particulièremen
accueilli
t
son
les
e
rapp
IMSc,
orteurs,
Je
Jean
les
Goubault-Larrecq
Cornelius
p
et
our
Lucan
sa
de
lecture
F
très
d'Informatique
atten
Ia³i
tiv
our
e
v
du
aidé
man
con
uscrit
uer
et
études
p
F
our
et
ses
e
remarques
mon
p
de
ertinen
en
tes,
p
et
m'a
Thomas
oir
Wilk
et
e
à
p
oursuivre
our
v
son
une
obser-
Je
v
Cédric
ation
ournet
qui
our
a
v
conduit
accepté
à
p
une
c
appro
son
c
e
he
Cen
alternativ
Comm
e
INRIA-Microsoft
du
h,
traitemen
à
t
nouv
de
collab
la
Ricardo
complexité
et
dans
Bharga
le
an
c
our
hapitre
patience
2
compréhension
et
endan
p
la
our
nale
a
la
v
de
oir
do
bien
t.
subi
je
une
mes
présen
c
tation
p
dans
leur
une
précieux
langue
endan
qui
ces
n'étais
années.
pas
Remerciemen
laiv.
.
1.2.2
able
.
des
.
matières
.
In
.
tro
.
duction
.
1
.
Proto
cryptographic
coles
.
cryptographiques
.
.
.
.
28
.
29
.
.
.
.
.
messages
.
.
.
.
.
On
.
P
.
.
.
dels
.
.
.
.
.
v
.
.
.
.
.
.
.
.
.
.
.
rewriting
.
.
.
.
.
.
.
.
.
A
.
.
9
.
1.1
36
Proto
.
coles
.
de
.
comm
Résultats
unication.
.
T
.
erminologie
23
.
cols
.
.
.
.
.
.
.
.
.
1.1.1
.
.
.
.
.
.
.
and
.
.
.
.
.
.
.
.
.
.
9
.
1.2
.
L'in
1.1.4
trus
.
.
.
.
T
.
.
.
.
.
.
.
Cryptographic
.
.
.
.
.
.
.
cryptographic
.
.
.
.
.
cryptographic
.
.
.
.
.
o
.
.
.
.
.
a
.
.
.
.
.
22
.
I
.
transfert
.
.
.
.
.
.
.
.
.
.
.
1
.
cryptographic
.
Preliminaries
.
.
.
.
.
.
10
.
1.3
.
Propriétés
.
de
.
sécurité
.
.
.
.
erms
.
order-sorted
.
.
.
.
.
.
.
.
.
.
.
P
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Substitutions
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
theories
.
.
11
.
1.4
.
Primitiv
.
es
32
cryptographiques
deduction
.
.
.
.
.
.
.
.
.
.
.
.
.
33
.
es
.
.
.
.
.
.
.
.
.
.
.
34
.
system
.
cols
.
.
.
.
.
.
.
.
.
signature
.
cols
.
.
12
.
1.5
.
A
.
ttaques
T
.
systems
.
cols
.
.
.
.
.
38
.
use
.
deduction
.
.
.
.
.
.
.
.
.
v
.
3.2
.
artie
.
I.
.
de
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Chapitre
.
Mo
.
for
.
proto
.
1.1
.
.
.
.
14
.
2
.
Analyse
.
de
.
proto
.
coles
.
cryptographiques
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
27
.
T
.
o
.
er
.
signatures
.
.
.
.
.
.
.
.
.
.
.
.
.
.
15
.
2.1
.
Vérication
.
sym
1.1.2
b
ositions
olique
subterms
de
.
proto
.
coles
.
de
.
sécurité
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
1.1.3
.
.
.
.
.
.
16
.
2.2
.
Lien
.
en
.
tre
.
les
.
appro
.
c
.
hes
.
sym
.
b
.
oliques
.
et
.
cryptographiques
30
.
Equational
.
and
.
systems
.
.
.
.
.
.
.
.
20
.
2.3
.
Résultats
.
de
.
décidabilité
1.1.5
et
erm
de
systems
transfert
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
1.2
.
primitiv
.
and
.
.
.
.
21
.
3
.
Con
.
tributions
.
and
.
plan
.
de
.
la
.
thèse
.
.
1.2.1
.
sort
.
for
.
proto
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
35
.
A
.
for
.
proto
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
21
.
3.1
1.2.3
P
w
artie
deduction
I.
for
Résultats
proto
de
.
décidabilité
.
.
.
.
.
.
.
.
.
.
1.2.4
.
the
.
of
.
third
.
system
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
41
.
T
..
.
.
able
.
des
.
matièr
.
es
.
1.2.5
.
The
.
deduction
.
problem
.
.
69
.
.
.
.
.
Horn
.
.
.
.
.
.
.
Correctness
.
.
.
.
.
.
.
erties
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
43
.
1.3
.
Roles
.
.
.
.
ermination
.
.
.
h
.
y
.
.
.
.
.
.
.
timestamps
.
.
.
.
.
.
.
results
.
.
.
.
.
clauses
.
.
.
.
.
.
.
83
.
.
.
.
.
constrain
.
.
.
.
.
.
.
rules
.
.
.
.
.
.
.
pro
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Completeness
.
.
43
.
1.3.1
.
Sp
.
ecication
time
of
.
roles
.
.
An
.
termination
.
.
.
ecialised
.
.
.
.
.
k
.
.
.
.
.
.
.
for
.
.
.
.
.
2.4
.
.
.
.
.
.
.
.
.
Chapitre
.
3.1
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
43
.
1.3.2
rom
Execution
.
of
.
roles
.
.
.
.
.
.
.
.
.
.
.
.
2.2
.
systems
.
.
.
.
.
.
.
.
.
.
.
.
.
2.2.1
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2.2.2
.
in
.
.
.
.
.
.
.
.
.
.
.
59
44
.
1.3.3
.
Executable
.
roles
.
.
.
.
.
.
.
.
.
.
61
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2.2.5
.
p
.
.
.
.
.
.
.
.
.
.
.
65
.
e
.
p
.
.
.
.
.
2.3
.
some
.
y
.
.
.
.
45
.
1.3.4
.
Roles
Detection
with
cycles
matc
.
hing
.
and
.
roles
.
with
.
equalit
.
y
2.3.2
tests
cols
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
46
.
1.4
.
Proto
.
cols
.
.
Decidabilit
.
Horn
.
mo
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
3.1.1
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
3.1.2
.
cols
.
.
.
.
.
.
.
.
.
.
.
.
.
T
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
47
.
1.4.1
56
Sp
Simplifying
ecication
t
of
.
proto
.
cols
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
57
.
Simplication
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
47
.
1.4.2
58
Execution
Decision
of
cedure
proto
NP-time
cols
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2.2.3
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
48
.
1.4.3
2.2.4
Executable
.
proto
.
cols
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
63
.
T
.
in
.
olynomial
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
49
.
P
2.2.6
art
alternativ
I
approac
Decidabilit
to
y
olynomial-time
results
.
51
.
Chapitre
.
2
.
Decidabilit
68
y
Decidabilit
results
of
using
sp
constrain
securit
t
prop
systems
.
2.1
.
The
.
mo
.
del
.
.
.
.
.
.
.
.
2.3.1
.
of
.
ey
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
69
.
Secrecy
.
proto
.
with
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
78
.
Conclusions
.
.
.
.
.
.
54
.
2.1.1
.
Constrain
.
t
.
systems
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
79
.
3
.
y
.
for
.
clauses
.
The
.
del
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
54
.
2.1.2
.
F
.
rom
.
proto
.
cols
.
to
.
constrain
81
t
Horn
systems
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
82
.
F
.
proto
54
to
2.1.3
clauses
Securit
.
y
.
prop
.
erties
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
vi
.
..
e
erties
A
.
fragmen
.
t
.
of
.
Horn
.
clauses
del
.
.
.
P
.
.
.
.
.
.
.
.
.
.
.
T
.
.
.
.
.
calculus
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
124
.
4.4
.
.
.
4.4.2
.
died)
.
.
.
simple
.
.
.
.
.
The
86
.
3.2.1
Mo
In
.
truder
.
clauses
.
.
.
.
.
.
.
.
.
.
frames
.
.
.
.
.
.
.
4.3.1
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
col
.
4.4.3
.
.
.
.
.
P
.
Chapitre
.
secrecy
.
.
.
.
.
.
.
.
86
.
3.2.2
.
Proto
.
col
.
clauses
.
.
within
.
.
.
109
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
secrecy
.
.
.
.
.
Generalisation
.
.
.
.
.
116
.
.
.
.
.
.
.
.
.
.
.
otheses
.
.
.
.
.
.
.
4.3.2
.
.
87
.
3.2.3
.
Extending
.
the
of
in
.
truder
.
p
.
o
cryptographic
w
.
er
.
.
ahalom
.
.
.
.
.
.
.
.
.
symmetric
.
.
.
.
.
rog
.
.
.
.
.
.
.
.
.
.
.
I
.
results
.
F
.
to
.
The
.
.
.
.
.
.
.
.
87
.
3.3
.
A
.
decidabilit
.
y
.
result
107
.
pi
.
.
.
.
.
.
.
.
.
.
.
.
.
107
.
proto
.
applied
.
.
.
.
.
.
.
Secrecy
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
112
.
e
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
89
4.2.1
3.3.1
strong
Ordered
.
resolution
.
.
.
.
.
.
114
.
w
.
.
.
.
.
.
.
.
.
.
.
A
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
h
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
89
result
3.3.2
.
Our
.
resolution
.
metho
.
d
.
.
.
.
.
.
.
.
Pro
.
termediate
.
.
.
.
.
.
.
.
.
.
.
.
.
to
.
cols
.
.
.
.
.
.
.
.
.
4.4.1
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
90
.
3.3.3
hro
A
ey
decidable
.
class
.
.
.
.
.
.
Mouthed
.
col
.
.
.
.
.
.
.
.
.
vii
.
.
.
.
.
.
.
.
.
102
.
art
.
I
.
ransfer
.
103
.
4
.
rom
.
secrecy
.
strong
.
4.1
.
mo
.
.
.
.
.
.
.
.
.
.
.
.
91
.
3.3.4
.
Examples
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
4.1.1
.
applied
.
calculus
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
4.1.2
.
deling
.
cols
.
the
.
pi
.
.
.
.
.
.
93
.
3.3.5
.
Pro
.
ofs
4.1.3
of
prop
in
.
termediate
.
results
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
4.2
.
assiv
.
case
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
94
.
3.4
.
Application
.
to
.
the
.
Needham-Sc
.
hro
.
eder
.
symmetric
.
k
.
ey
114
proto
Simple
col
implies
.
secrecy
.
.
.
.
.
.
.
.
.
.
.
.
.
.
98
.
3.4.1
.
Presen
4.2.2
tation
of
of
ell-formed
the
.
proto
.
col
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
4.3
.
ctiv
.
case
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
98
.
3.4.2
.
Correcting
.
the
.
proto
.
col
120
.
Our
.
yp
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
120
.
Main
.
.
.
.
.
.
.
.
.
.
.
.
.
.
99
.
3.4.3
.
A
.
transformation
.
preserving
.
secrecy
.
.
.
.
.
.
.
.
.
.
4.3.3
.
ofs
.
in
.
results
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
99
125
3.4.4
Application
Secrecy
some
of
proto
the
.
corrected
.
proto
.
col
.
.
.
.
.
.
.
.
.
.
.
.
128
.
Y
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
102
.
3.5
.
Conclusions
.
.
128
.
Needham-Sc
.
eder
.
k
.
proto
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
129
.
Wide
.
F
.
Proto
.
(mo
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
130
.
3.2
..
.
.
able
.
des
.
matièr
.
es
.
4.5
.
Conclusions
.
.
traces
.
.
.
.
.
.
.
theorem
.
.
.
.
.
p
.
.
.
.
.
.
.
142
.
.
.
ransference
.
.
.
executions
.
.
.
Pro
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
5.5.1
.
.
.
.
.
.
.
securit
.
.
.
.
.
.
.
.
131
.
Chapitre
.
5
.
A
.
transformation
.
for
.
obtaining
.
secure
h
proto
.
cols
.
5.1
pro
Comparison
.
with
.
Katz
.
and
.
Y
.
ung's
.
compiler
.
.
.
.
.
.
Bibliographie
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
single
.
.
.
.
.
.
.
.
.
.
.
.
.
T
135
prop
5.2
.
The
.
mo
.
del
.
.
.
.
5.5.3
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
5.5.4
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
144
.
sk
.
the
.
.
.
.
.
.
.
.
.
5.5.6
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
5.6
.
.
.
.
.
.
136
.
5.3
.
Securit
.
y
.
prop
.
erties
.
.
Conclusions
.
ectiv
.
viii
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
142
.
Honest,
.
session
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
138
5.5.2
5.3.1
ransferable
A
y
logic
erties
for
.
securit
.
y
.
prop
.
erties
.
.
.
.
.
.
.
.
.
.
.
.
143
.
T
.
theorem
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
143
138
Honest
5.3.2
.
Examples
.
of
.
securit
.
y
.
prop
.
erties
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
5.5.5
.
of
.
etc
.
of
.
transference
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
145
140
Detailed
5.4
ofs
T
.
ransformation
.
of
.
proto
.
cols
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
146
.
Conclusions
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
141
.
5.5
.
T
150
ransfer
and
result
ersp
.
es
.
157
.
T
.t.
m'app
ils
tro
participan
duction
9
Les
t
proto
(
coles
(abréviations
de
session
comm
des
unication
Un
son
p
t
est
omniprésen
le
ts
initiateur
de
génériques
nos
pièces
jours.
obtenan
Ils
In
son
qu'ils
t
1.1
essen
celui
tiels
eut
p
.
our
connaissance.
le
c
fonctionnemen
e
t
l'exp
correct
Ici
d'un
.
large
côté
nom
l'initiateur
bre
de
d'applications
des
impliquan
égalemen
t
r
des
par
disp
réaliser
ositifs
sécurité
électroniques
buts
comm
1
unican
comm
ts.
comm
Ils
p
son
première
t
suit
ainsi
je
présen
ou
ts
Enc
dans
e
nos
r
activités
l'
main
première
tenan
la
t
o
comm
proto
unes,
certain
comme
a
com-
r
m
oles
uniquer
et
à
son
l'aide
les
d'un
ondeur
téléphone
on
mobile,
cette
écrire
obtenir
des
parlan
message
Nous
électroniques,
t
ou
fait
faire
participan
des
Il
ac
t
hats
t
sur
analyses
l'In
coles
ternet,
d'être
ou
t
encore
our
s'ab
t
onner
coles
aux
coles
c
T
haînes
cole
de
simple
télévision
quand
pa
se
y
our
an
et
tes.
décrire
Dans
.
b

eaucoup
elle
de
souv
telles

applications,
agents
la

sécurité
On
est
proto
d'une
suite
imp
gles
ortance
indiquan
ma
é
jeure.
dans
On
le
v
égalemen
eut
règle),
que
en
nos
é
comm
Dans
unications
c
soien
joue
t
ôle
priv
y
ées,
:
que
et
nos
ondeur
données
sym
ne
et
soien
our
t
dans
pas
des
mo
des
diées
dénoten
p
tités
endan
du
t
ectiv
leur
situations
transmission,
b
on
oncr
v
(c'est-à-dire,
eut
p
être
séquence
sûr
éc
de
ainsi
l'iden
proto
tité
ouv
de
concrétiser
notre
certain
partenaire
de
de
session
comm
.
unication.
génériques
Des
distribué.
proto
est
coles
conséquen
de
très
sécurité
ortan
son
de
t
des
alors
soigneuses
construits
proto
p
de
our
an
assurer
sûr
de
réalisen
tels
les
buts,
p
et
lesquels
ils
son
emploien
conçus.
t
Proto
la
cryptographiques
cryptographie
Proto
p
de
our
unication.
obtenir
erminologie
les
proto
briques
de
de
unication
base.
est
Cep
utilisé
endan
deux
t,
ersonnes
même
réunissen
si
p
ces
la
briques
fois,
son
p
t
le
parfaitemen
comme
t
:
sûrs,
arties
la
t)
manière
Bonjour,
don
m'app
t
en
elles

son
(moins
t
,
com
Je
binées
elle
an
.
d'obtenir
han
un
de
proto

cole
observ
est
qu'un
très
cole
imp
une
ortan
de
te.
è
En
,
eet,
hacune
b
t
eaucoup
exp
de
diteur
proto
t
coles
la
qu'on
règle),
a
destinatair
considéré
(
corrects
dans
se
deuxième
son
et
t
message
a
v
v
y
érés
par
a
éditeur.
v
un
oir
cole
des
haque
failles
t
(pas
un
du
r
tout
.
liées
il
à
en
la
deux
cryptanalyse).
le
Ces
t
failles
le
p
ép
euv
ellen
en
Les
t
b
être
s'app
emplo
concrets,
y
p
ées
Alice
par
Bob)
des
le
en
droit
tités
règles
malv
t
eillan
noms
tes,
qui
et
t
p
iden
euv
de
en
et
t
rép
en
resp
traîner
emen
des
En
conséquences
concrètes,
très
a
négativ
esoin
es
c
une
étiser
fois
description
que
les
le
génériques)
proto
our
cole
la
est
réelle
déjà
messages
déplo
hangés,
y
t
é,
d'une
car
du
la
cole.
même
p
faille
ons
p
t
eut
seulemen
être
un
emplo
rôle
y
t
ée
ce
à
une
plusieurs
d'un
reprises
ôle
jusqu'à
Les
ce
ts,
qu'une
ou
correction
est
imp
A⇒ B : A
B ⇒ A : B
A
B
A
B A B

Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.

Diffusez cette publication

Vous aimerez aussi