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

Eugen Zalinescu

Description

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

Informations

• Publié par: Thesee
• Nombre de lectures: 42
• Langue: Français
• Poids de l'ouvrage: 1 Mo

Extrait

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 : [e-mail]




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<