Analyse Formelle d'un Protocole de Vote Cyrille Wiedling

Publié par

Master, Supérieur, Master
  • cours - matière potentielle : du temps
  • cours - matière potentielle : l' année
  • mémoire
  • mémoire - matière potentielle : stage directrice de stage
Université de Strasbourg UFR de Mathématiques & Informatique Master 2 Calcul Scientifique & Sécurité Informatique Mémoire de Stage Directrice de Stage : V. Cortier, CNRS, LORIA Lieu du Stage : LORIA, Equipe CASSIS Analyse Formelle d'un Protocole de Vote Cyrille Wiedling <> Strasbourg, 1 er Août 2011
  • preuve de décidabilité pour la déduction
  • nb chiffré avec la clef publique
  • mémoire de stage directrice de stage
  • bob
  • générateur de reçus
  • urnes
  • urne
  • protocole
  • protocoles
  • stage
  • stages
  • vote
  • votes
Publié le : mercredi 28 mars 2012
Lecture(s) : 41
Source : loria.fr
Nombre de pages : 72
Voir plus Voir moins

ormelle
:
2
Wiedling
LORIA
Informatique
e
UFR
de
Scien
1
Sécurité
&
du
ourg
,
Master
Analyse
de
Proto
Calcul
ote
de
Strasb
tique
oût
,
Lieu
ersité
Strasb
Mathématiques
&
CNRS
Informatique
Stage
Mémoire
LORIA
de
Equip
St
CASSIS
a
F
ge
d'un
Directrice
cole
de
V
Stage
Cyrille
:
<zell.cyrillew@cegetel.net>
V.
ourg,
Cor
A
tier
2011
,
Univ
er.
3.3.2
.
.
.
.
.
.
.
.
.
.
.
2
.
25
.
34
ote
.
.
.
.
.
.
an
.
2.1.2
ote
.
.
.
.
.
.
.
.
.
.
.
Préliminaires
.
.
.
Enoncé
.
.
.
.
.
.
.
du
.
.
.
.
alences
.
.
Générale
F
.
.
.
du
13
.
.
.
.
.
.
.
2.2
.
et
4.1
.
.
1
.
Systèmes
.
.
our
.
.
.
.
15
.
2.1
.
.
.
duction
.
.
.
.
.
.
.
.
.
.
.
.
18
2.1.1
.
.
.
.
.
.
Appliqué
.
.
.
.
.
6
.
.
.
.
.
et
coles
.
.
.
.
.
21
.
égien
.
.
.
.
.
e
.
.
.
.
.
.
.
.
.
.
8
.
.
.
.
t
.
.
.
.
.
.
.
Décidabilité
.
.
.
.
e
.
Norv
du
.
Norv
.
.
.
.
.
.
.
.
8
V
.
.
6
.
.
.
Asso
.
.
.
.
.
.
.
Proto
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Syn
.
Appliqué
ermes
.
.
.
.
.
.
.
.
3.1.2
.
du
.
.
.
.
.
.
.
.
3.1.3
.
.
.
.
.
.
.
.
Présen
.
.
.
.
.
s,
21
.
des
clos
e
.
.
.
.
.
.
.
.
.
.
.
Mo
.
cole
.
.
.
.
Substitutions
.
.
.
.
.
.
3.3.1
.
.
.
.
.
.
.
.
.
.
.
.
.
2
texte
délisation
.
.
.
.
.
.
.
.
Équationelles
.
Proto
.
.
.
.
A
.
assif
.
Équationelle
.
.
.
.
.
.
.
.
.
.
.
32
.
la
.
.
14
.
Proto
.
Rééc
.
.
.
.
.
.
Conden
.
ote
.
Proto
.
37
de
.
.
.
.
.
.
.
tro
.
.
.
.
.
.
.
In
5.1.1
Systèmes
Simpliée
Préliminaires
.
.
.
Con
.
.
.
ermes
.
.
37
In
Résultat
.
.
.
.
.
.
.
.
.
.
aux
.
.
5.2
.
.
.
.
coles
.
.
.
.
.
.
.
.
.
.
.
.
38
.
.
.
.
.
.
duction
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
3.1.1
11
taxe
.
Pi-Calcul
T
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
18
.
Sém
.
tique
.
Pi-Calcul
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
20
.
Equiv
.
.
.
.
.
.
.
.
.
.
.
.
1.2
.
.
.
.
.
.
.
tation
.
11
.
.
.
Sous-terme
.
.
.
taille
3.2
.
ormalisation
termes
proto
.
d
.
v
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Con
.
.
.
.
3.3
.
délisation
.
Proto
.
Norv
.
.
.
.
.
.
2.1.3
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2
.
Théori
.
Équationelle
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
2
In
Mo
.
.
.
.
.
.
.
.
.
.
.
.
13
.
.
.
Théories
.
1.3
.
.
.
.
.
.
.
cole
.
.
.
.
4
.
ttaquan
Descriptions
P
.
32
.
Théorie
.
Simpliée
.
.
.
.
.
.
.
.
.
.
.
.
5
.
.
.
.
.
.
.
.
.
.
4.2
.
de
.
Déduction
Le
.
.
.
.
.
2.3
.
.
.
de
.
.
.
ritur
.
cole
.
.
.
.
.
.
.
.
5
.
tialité
.
V
.
p
égien
le
.
cole
.
égien
.
5.1
.
.
.
.
.
.
.
.
V
.
.
.
.
.
.
.
des
.
.
.
.
.
.
.
par
.
.
.
.
.
.
.
4
37
2.4
Une
2
ersion
d'Inférence
.
ternet
.
.
.
11
.
.
.
.
.
.
.
T
.
.
.
1.1
.
.
.
et
.
.
5.1.2
tribution
du
.
.
ciés
.
.
.
tro
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
able
matières
4
.
.
.
.
.
.
.
.
.
37
.
Notations
.
.
16
.
3
.
Mo
.
délisation
.
en
.
Pi-Calcul
.
Appliqué
.
18
.
3.1
.
Présen
.
tation
.
.
.
.
.
.
.
.
.
.
.
.
2
.
T.
.
.
51
la
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
A
.
57
.
.
.
.
48
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Chap
.
d
.
.
5.3
.
42
.
.
.
.
.
.
.
Notes
.
délisation
.
.
.
.
.
.
.
.
.
.
.
.
.
6.3
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
Conclusion
.
es
.
re
.
Preuv
.
Chapitre
39
.
.
.
.
.
.
.
Equiv
.
5.4
.
.
.
.
Statique
.
.
.
.
.
.
.
.
6.2
.
sur
.
mo
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
48
.
Résultats
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
olutions
.
.
.
.
Ev
partielles
.
.
alence
Relation
.
.
.
44
.
6
.
ProV
.
erif
.
48
.
6.1
49
A
50
Prop
Preuv
os
du
de
it
ProV
4
erif
B
.
es
.
u
.
5
.
3
.
5.2.1en
utilisateurs
t
système,
le
t
naïf
t
de
ersonnes
formaliser
que
;
certain
Dans
e
s'in
la
unications
examiner
cteurs,
présence
jouer
mo
t
faire
t,
pas
comme
réseaux
v
cours
?
d
Il
donnen
o
y
réseau
manière
son
nous
formalisan
t
malhonnêtes
téléphone
r
roto
consiste,
in
mathématique,
es-ci.
un
des
c
ac
es
our
si
de
p
utilisen
à
ou
A
coles
t
[DLMS99].
face
ymat
le
de
parfois
son
r
de
tous
gestionnaires
eu
honnêtes.
emen
que
vraimen
honnêtes.
coles
d'en
fonctionnen
quelques
une
t
des
coles,
des
de
en
t
elles
ainsi
partie
robustes,
eectuer
Con
la
d'une
e
d-
la
p
er
hine
v
v
se
les
p
démon
même
à
?
tec
dév
ec
des-
e
etc...
p
il
tra
étudier,
mélanger
t
ers
men
proto
.
nos
sécurité
s
même
et
tes,
olué
sans
ec
notre
temps,
préserv
face
est
sait
que
on
réseau
es
tous
vie
même
comme
e
v
que
satisfaction,
réseau
jours,
t
p
serait
sans
p
t
concepteurs
des
t
à
en
des
ma
t
eux
our
mais
rée
p
jours,
faire
La
dégâts.
:
les
coles
p
des
ommen
série
participan
handises
euv
deux
y
en
her
une
elopp
in
proto
ces
e
hnologies,
tric
nécessiten
L'analyse
paris
partan
de
écication
prép
le
our
en
p
par
de
e
h
d'une
tout,
café
ligne,
ni,
de
t
i
lemen
un
que
bancaires
he
qu'il
puis
t
v
des
de
oter
Diéren
au
d'analyse
t
a
ées
élections.
proto
p
au
plus
l'authen
s
l'étude
sonne
proto
n
en
t
sait
v
i
vraimen
des
t
es
compte.
c
ces
la
de
hac
coles
ourtan
coles
de
il
tels
informatiques
dicile
on
de
v
con
év
reste
non
t
au
être
vies,
que
du
anon
à
soit
tout
é
le
Il
monde
naïf
.
croire
commen
les
nos
d'un
l
informatique
la
t
utilise
honnêtes.
é
est
et,
naïf
de
p
ils
ns
même
r
t
les
les
du
p
s
elopp
n
de
tous
il
Il
ersonnes
même
t
de
téressen
enser
a
les
encore
du
t
étaien
t
tous
proto
Bien
la
tendu,
que
grande
don
jorité
p
tre
ils
le
comm
t,
t
les
quasimen
autres
llemen
euv
duction
t
.
énormémen
tout
de
plupart
En
et
t
proto
proto
commander
on
réalisen
eut
nous
c
une
t
marc
s
d'actions
ts
nouv
p
tre
en
par
essa
a
er
place
tric
mais
et
ou
dév
grande
e
tec
des
de
coles
ternet,
même
p
n
r
de
coles
heurs.
des
texte
t
formelle
les
en
présence
t
ou
sp
p
d'un
les
à
p
mo
au
éliser
assurer
langage
teractions
comme
sécurité
exem
ok
l
cell
la
nd
délisation
Après
mac
en
à
en
par
umaines
automate
errions-nous
a
réaliser
an
l'argen
d'en
ondéran
éga
à
t
transactions
propriétés
étranger
l'on
fon
herc
our
à
ou
trer,
nous
d'en
ons
la
hète
érication
v
l'aide
biens
preuv
de
mathématiques.
Jouerions-nous
tes
p
hniques
p
formell
on
er
été
des
elopp
v
p
en
des
une
coles
P
tinés
ersonne
paiemen
éritablemen
à
nou
tication,
r
Dans
ne
formelle
au
ces
ouvio
coles,
ne
y
s
a
dans
l'on
le
bien
ense
car
oir
ls
v
t
e
primitiv
simples
tro
De
proto
te
v
plus
our
ok
e
distribuer
le
les
hire-
cartes
t,
?
signature
A
le
ccepterions-nous
hage
d'en
P
v
t,
o
problème
y
la
er
de
notre
proto-
v
reste
ote
car
par
sous
c

ourr
ères
i
train
er
il
au
indécidable
Gouv
4
ernemen
Ine
stage,
des
Norv
que
No
Un
la
On
dans
pro
proto
t
déduction
souv
l'outil
démon
propriété
tan
démon
Il
une
ProV
la
[DKR09],
v
tes
v
our
er
c
en
du
à
une
en
ers
formelle
érier
tiv
l
visageable
ios
p
légèremen
exemple,
décidabilité
es
de
ec
t
F
p
ermis
de
son
l
consacré
concerne
in
F
notions
récemmen
in
t
cole
disp
déci
coles
ée
test
osera
de

mo
dernier
résultats
proto
oir
a
été
tel
t
classe
néanmoins
est
qui
c'est
est
celle
t
été
proto
dans
problème
du
tiellemen
une
de
déduction
[ABB
e
à
cole
à
résultat
des

outils
tec
amoto
p
de
Le
même
le
très
globalité
t
des
deuxième
tribution
i
proto
our
le
mo
es
de
mis
nécessaire
...)
troisi
implémen
le
nom
formelle
source
Norv
ourtan
sur
ternet,
i
he
une
i
é
éc
cinquième
etites
ail
i
de
Nous
de
de
Le
ce
tera
Plusieurs
que
p
n
l
en
analyse
et
û
un
tialité
ossible
elopp
temps
de
v
augm
et
plus
aussi
our
de
t
une
restrein
inspirée
s
sur
érication
qui
disp
p
exp
cette
étudier
con
comme,
simplié
leur
cole
rép
égalemen
donc
e
VISP
our
des
ciée
a
équati
men
dériv
05]
du
main,
v
et
n.
cas
in
[Bla01].
la
coles
décidabilité
nom
est
a,
de
t
mettre
Oh
t
e
d'analyse
d'Helios
c
yser
mémoire
c
cole
(Les
dans
souv
présen
breux
sc
ardues.
coles
action.
c
hapitre
certiés

ce
imp
th
nécessaires
particulièremen
à
JFK
à
cole
formelle
our
ap
Norv
ble
Keying)
aura
place
maîtriser
y
stage.
[Gjo10],
c
de
ro
et
appliqué
En
mo
co
du
attaques.
v
actuellemen
Le
une
p
sur
résultat
les
a
t
de
très
ciée
é
ersion
v
la
de
uati
e
cole.
de
hapitre
en
tra
unes
de
ce
preuv
v
conden
t
proto
osons
ote
plus
ersion
formelle
me
outils
hapitre
to
n
le
erif
appliqué
application
En
Norv
p
tra
on
résultats
faire
t
mo
an
et
limites.
n'est
NP-complet
la
de
souv
est
v
de
t
solution
l'utilisation
olynomial
é
problèm
primi-
t
en
noté
es
ce
p
m
complexes
que
en
autres
excluen
c
automatiser
.
l'utilisation
preuv
un
ad-mano,
outil
de
v
réalisée
don
Hél
t
[CS11],
on
a
des
réalisée
ose
our
de
trer
our
propriété
coles
un
le
texte
onen
t
de
vis-à-vis
par
proto
sécurité.
global.
NP-compl
fournit
est
t
A
preuv
nécessaire
de
t
p
réaliser
la
A
asso
preuv
à
ondre
théorie
directe-
on
NP
lle
t
ée
v
celle
la
proto
ou
de
comme
ote
t
égie
les
Ce
erif
est
d'étude
téressan
le
dans
proto
mesure
Ces
la
de
de
c
déduction
ujiok
une
on
hnique
Ok
base
bre
our
et
au
p
oin
ta
des
1
cédures
ou
automatique.
d'anal-
premier
[CS11],
hapitre
celles-ci.
ce
si
décrira
de
proto
elles-ci
de
problème
ote
t
sa
nom
et
en
tera
alg
e
plus
héma
proto
proto
Con
qu'il
en
La
Le
(mails
c
on
sera
i
aux
de
n
[AB03],
tions
mémoire
ortan
p
et
tout
p
cole
commencer
t
s'
m
téresser
proto
la
(Just
délisation
de
des
T03].
coles,
ote
erçu
ast
l'ensem
égien
des
a
qu'il
en
été
[ABF04],
de
très
p
un
ce
t
Le
et
ème
déjà
hapitre
an
t

duira
trouv
pi-calcul
don
ainsi
sessions,
la
le
délisation
des
complète
de
proto
alors
de
est
ote
P
égien.
t
quatrième
bre
hapitre
onible
ortera
t
le
In
de
fâc
d
apparemmen
b
proto
lité
encore
la
particulier,
asso
p
à
de
v
r
dériv
us
de
o
théorie
otes
q
de
onelle
limité
proto
sur
Le
happ
c
p
exp
tendance
le
comm
v
t
principal
de
ce
bre
la
r
e
en
la
ège.
tiali
ne
du
prop
cole
à
v
une
dans
sessions,
v
délisation
simpliée.
tels
sixiè
de
et
terminer.)
c
pro-
présen
ou
rapideme
cole
t
l
ProV
pi-calcul
ainsi
généraux.
son
[AF01]
au
outils
cole
our
égie
eet,
au
ouv
v
co
de
en
qui
eur
illustren
une
les
t
v
formelle
tages
délisation
les
ainsi
1.
problème
problème
trer
est
demande
problème
conden
décision
dév
qu'il
des
p
en
v
sous
nom
de
[R
que
or
coles
tributions
met
otes.
une
Comme
en
les
p
autres
(La
proto
des
coles
es
de
érian
v
cette
ote,
est
il
NP)
éc
que
happ
problème
e
au
lui
oins
aussi
dicile
à
tous
la
es
v
problèmes
érication
la
automatisée
lasse
et
5
donc
Même
+plit
hro
cole
r
i
an
l'en
l
es,

En
mais
exécutée
a
une
deux
articip
uniquen
cole
tous
imp
une
a
gâteau),
proto
our
Ce
et
n'est
[Sc
V
e
proto
un
fournir
ee
é
plusieurs
p
deux
aux
au
le
he.
est
Norv
(A)
y
es
d'une
(par
,
pas
d'étude

une
une
faire
qu'il
à
Proto
pas
étap
oto
de
erte
et
exem
oto
v
être
Nee
but
proto
précéden
m
impliquan
t
deux
à
que
étap
qu'il
ec
p
s'assurer
our
puisqu'i
In
on
une
proto
v
ts
dénition
r
v
deux
te.
eut
n
e
question
our
Ce
tâc
d'étap
cuire
le
ce
à-dire
proto
c
lieu,
ole
onçu
stage.
c
i

cole
es
c
duction
ressem
un
proto
le
n'accompli
n.
tâc
Dénition
un
doit
mais
p
une
son
temps.
Un
ci
autre
l
cole
ec
p
te
ole
e
a
ham
ote
[NS78].
que
est
d'étap
authen
ne
en
temps,
comm
L'expression
un
deux
d'un
plusieurs
oi,
présen
consiste

La
ts,
b
au
a
prot
com
ersonnes
ts
accom
p
un
tâc
Norv
et
une
p
de
oir,
tâc
le
tra

Cette
:
ote
d'une
est
e
ternet
en
ortan
ts,
égie
Bob
Il
réaliser
ers
séri
est
d'étap
qui
p
d'une
accompli
égien
une
série
he
été
exemple,
es
un
appro
mais
c'est-
message
sujet
un
qu'un
cole.
c
dernier
c
l'expression
du
c
est
p
he
ac
su
omplir
1.1
tâche
te
indique
proto
d'étap
doit
tro
quelque
et
hose.
générale,
qui
a
ble
aux
un
début
cole
a
qui
une
t
coles
une
Chaque
he
concept
pas
e
pr
1.1.
cole
être
b
V
en
à
p
h96]
de
tour
Exemple.
proto
oi
aucune
un
pr
p
étap
e
our
v
ne
une
c
arian
eut
du
dans
col
exécutée
de
est
d
v
-Sc
cole
eder
t
Ce
série
cole
la
sensé
premier
une
te
tication
es,
utuelle
soit
tre
de
parties
ctuée.
uniquan
t
sur

r
ainsi
seau.
ou
Bob,
ou
d'Alice
p
v
par
à
ants
e
participan
première
indique
ersonne.
le
onne
faut
la
conçue
v
moins
t
ter,
m
p
qu'ils
our
de
p
participan
o
ermet
accomplir
l
p
he
proto
une
Le
accom-
;
Comme
ir
eut
1
Proto
de
hapitre
assez
In
ordonnée
qu'un
p
v
ersonne
ce
isolée
co
ne
réunit
p
les
eut
ingrédien
accomplir

un
il
proto
constitué
cole

.
i
Il
d'étap
est
met
vrai
scène
qu'une
participan
p
Alice
ersonne
et
seule
(B),
p
6
n'est
Chapitre
A! B : fA;N gA pub(B)
B! A : fN ;N gA B pub(A)
A! B : fN g :B pub(B)don
uniquer
dup
hirer
v
tâc
un
nom
l'a
r
'
que
a
hiré
publique
d'initier

t
v
v
p
,
v
a
c
bre
Alice
c
Elle
v
ors
ne
cette
à
lieu,
vulnérable
elle,
v
clef
une
nom
aléatoire,
passer
Si
n
y
la
v
au
de
comm
Bob
v
c
con-
Regardons
la
ren
t
eut
certain
ensera
C'est
o
st
comm
t,
l'en
v
qu'Alice
toujours
Mallory
et
en
t
v
hire
ersation
de
v
ée
a
au
allory
priv
qu'elle
e
elle,
tenan
est
sur
ice
a
le
Mallory
er
son
hiré
d'initier
seuls.
ob
B
elle
rien,
Après
p
er
ec
bre
proto
con
à
autre
être
a
t
ec
hiré
l'attaque
Mallory
ce
e
l
ce
un
cole
lequel
.
et
[Lo
bre
u-
lui
à
v
ce
clef
noter
Mallory
hiré
découvrir
proto
er
ssage
sa
t
A
la
elle
réaliser
v
Bob
de
En
En
Alice
a
il
A
clef
con
une
v
message
Alice
yp
à
nom
c
t
ec
sa
de

con
Bob
iden
ersonne
ainsi
reconnait
aléatoire
t
Mallory
la
le
une
se
qu'e
our
iden
de
à
déc
imp
et
v
o
p
Bob
Bob
oir
Alice
v
à
lef
session
que
bre
ce
elle,
qui
lui
t
e
a
l'iden
message
la
qu'Alice
son
a
message
Il
et
suivre
et
et
r
y
ai
,
v
p
qu'il
un
a
t
ec
son
vien
ne
ommen
v
clef
publique
déroule
qui
déc
y
l
an
oie
seconde
à
l'iden
nalemen
mo
qu'elle
puisse
hirer
ce
reconnaîtra
déc
un
qui
qu'elle
l
le
w
Mallory
tout
a
découv
n
bien
er
17
hiré
éditrice,
c
cette
a
Alice.
de
Malheureusemen
a
me
ouv
ce
en
a
o
cole
Bob,
Alice,
v
parvien
publique,
ec
à
pas
n
grâce
Bob
à
mais
clef
ec
sa
a
ec
comm
he.
train
d'Alice.
est
ee
premier
sa
Mallory
,
con
déc
aincu
est
lice
un
une
à
v
ce
a
attaque
ec
priv
ainsi
t
en
a
oie
e
Mallory
con
message
rencon
hiré
ec
v
re
la
,
publique
milieu
M
clef
,

tenan
bre
son
p
tité
ée,
,
p
qu'un
en
bre
u
sait
le
.
en
,
a
t
er
but
bre
Alice
autre
faire
oie
p
son
Al
lle
auprès
tité.
Bob,
:
a
un
hirer
en
message
osteur,
l'e
Alice
v
(M),
y
o
à
eut
après
t
v
ersuader
c
é
a
(A)
ec
nom
c
une
publique,
B
d'eux
a
us
.
de
ec
dernier.
et
ob,
alors
n'est
aléatoire
couran
p
de
ren
v
ut
déc
clef
le
e
et
oie
enser
y
désire
tité
uniquer
le
v
nom
lui.
à
v
a
donc
(B)
le
aléatoi
cole
le
ren
un
o
v
er
e
Mallory
n
qu
tité
il
re
ense
hiré
Alice,
discute
message
qu'il
tenan
v
conn
v
et
Alice.
nom
oir
son
c
c
la
a
t
ec
t
clef
se
d'Alice.
publique
,
:
ne
eut
ra
hirer
Bob
message,
en
e
générer,
v
étap
te
que
quel
la
Alice.
et
reçoit
dian
t
dernier
message
en
p
t
déc
proto
dans
être
elle
orrigé
et
l'exp
et
a
autre
qu'i
lui
w95]
p
Le
être
e
nom
comm
de
Lo
.
hiré
v
erte.
donc
nique
re
être
v
e
y
années
ec
a
c
mis
a
de
e
attaque
la
ec
publique
que
uniquer
c
.
hiré
v
publique
de
reçu
de
de
joutan
p
de
v
t
al
téressan
p
in
oir
est
train
Il
et
Bob.
v
de
y
auprès
à
tité
c
iden
a
son
ec
é
clef
dérob
est
a
tort,
dernière
.
cette
la
que
de
pas
attaque,
sait
croit,
ne
7
de
c
NA
N NA B
fA;N gA pub(M)
!A M
fA;N gA pub(B)
!M B
fN ;N gA B pub(A)
M B
fN ;N gA B pub(A)
A M
fN gB pub(M)
A! M
fN gB pub(B)
M! B
A NA
pub(B)
N NA B
N NA B
NB
pub(M) NB
pub(B)
N NA B
A! B : fA;N gA pub(B)
B! A : fB;N ;N gA B pub(A)
A! B : fN g :B pub(B)cédure
l'auditeur
électron-
en
ts
puisse
Proto
l'année
site
s'il
son
la
ote
otes,
d'utiliser
ni
papier
ses
de
t
virtuel.
ts
Il
scène
d'a
ote
de
dans
bleu
se
to
normalemen
reçus
qu'il
s'assurer,
au
le
soumettre
(Figure
v
tre
égien
1.
bureau
www.ev
en
Représen
égalemen
proto
m
col
exemple
t
par
our
y
m
infrastructure
t
comme
ote
retrouv
le
a
il
qui
en
les
ermettre
classique,
le
hireur
ctuellemen
le
oter
r
p
générateur
ote,
t
é
On
prédominan
héma
cours
diéren
t
lors
proto
v
à
taires
s'il
trouv
v
.
sur
1.1
p
des
re
ts
rev
Plus
présen
ce
désire
met
été
v
c
qui
p
(P)
ou
son
,
une
eu
en
l'élection.
me
comp
du
participan
pro
mon
lo
1.1.
cas,
dans
Il
les
r
re
[Gjo10].
l'urne
st
a

k
Il
ts
p
une
prévu
générateur
un
le
que
et
ote
don
t
est
propre
p
manière
ori,
déplo
ni
de
reçus,
p
hireur
v
hé.
en
et
t
e
bulletin
le
sur
des
phase
hanges
o
messages
de
participan
e
la
tation
soumission
ique
par
2012
informations
un
euv
test
t
de
sur
donne
ternet
ote
in
est
Figure
L'utilisateur

tiè
tation
eut
diéren
plusieurs
participan
t
du
satisfaction.
cole.
oter
précisém
cole
t,
le
proto
a
e
(par
en
unicipalités
un
s'il
otan
créé
(V)
hange
utilise

ordinateur
vis
p
Scytl
soumettre
s'il
v
our
à
a
infrastructure
une
ise
un
place
our
roblè
Cette
espagnole
est
duran
osée
élections
plusieurs
la
ts
v
le
cédure),
tre
dans
gure
ce
On
électronique.
e
seul
l'encart
cales,
clair
dernie
qu
est
t
v
participan
v
:
e
(B),
n
v
prit
s
est
c
compte.
er
p
diéren
est
v
A
comme
t
urne
à
le
par
de
ossible
(R),
système
déc
électeur
(D)
l'électeur
enn
Le
(A)
égalemen
t
son
rôle
v
de
soit
a
de
oste
ordinateur
i
classique
que
t
l'urne,
bureau
le
ersonnel
de
v
ni
y
déc
son
n'on
our
tric
ote
1.3
Norv
cole
étan
Descriptions
un
retrouv
alors
ci-dessous
au
1.2),
t
sc
de
simplié
tous
éc
des
Présen
Générale
de
1
des
compagnie
p
p
v
ts
otes
en
électroniques,
les
même
ts
si
de
ceux-ci
pro
on
de
t
d'un
eu
ote
lieu
un
après
Des
la
complémen
soumissi
p
on
en
du
ê
v
re
ote
ée
papier.
le
alg.dep.no
8
1.2
V P B D
R Aa
du

r
de
reste
table
le
plusieurs
otan
les
à
e
l'urne
s'il
ote
de
otes
et
étée
phase
ote
que
ce
le
au
de
c
après
pro
:
a
a
décom
p
i
on.
but
t)
l'
alen
ordinateur,
réceptionné.)
messages
désiran
v
à
v
destination
reçus,
quelques
donner
de
b
v
désire
via,
il
tran
compte
exemple,
transmet
sur
v
fait
reçoit
exemple
v
une
que
nateur
compte
Figure
qui
p
érier
son
ompte
a
t
à
(unique
v
s
rev
et
l'urne.
ermettan
jeu
v
hanges
est
est
haque
t
v
déc
otan
soumission
du
temps
hiré
Le
générateur
et
çus.
v
érications
Une
le
son
pro
générateur
reçus
ote
exp
as
otan

exempl
même
en
une
reçu
prise
dans
v
terv
qui
particulie
son
(P
érication,
site
t.
de
ni
sécurisé
deux
lors
conrmation
et
t
te
indiquan
son
v
a
pris
eectuer
un
t,
de
proto
a
ote
de
l
le
phase
en
L'ordinateur
le
c
v
c
ose
(V
corresp
hirer
v
dans
tre
puis
ts
cole
ossible
édier
reçus
Figure
lui
dernière
ainsi
qui
comparer
Ec
au
écoulé,
étap
de
é
hireur
our
duran
otan
ote
soumettre
la
ou
l'urne
par
de
si
de
partir
d'un
v
le
c
ote.
à
le
du
v
de
le
e
t
Après
fois
v
a
sur
de
message,
à
générateur
on.)
reçus
ordinateur
duit
l
fameux
v
qu'il
le
a
qu'il
édier
le
1.3.)
e
t,
p
par
e
e,
En
-
temps,
réceptionné
fournit
l'en
conrmation
enir
la
t
en
le
du
un
ote
générateur
l'urne
hamp
la
ar
à
r
tour,
in
v
un
au
cessus.
otan
w
Ce
otan
r
b
er
du
donc
par
messages
qui
une
-
pro
erreur
enan
v
de
reçus.
lui
autoriser
t
eu
son
ordi-
ote
p
été
à
en
y
et
le
reçu
en
générateur
du
reçus
ou
v
cole
lui
de
ermettre
our
v
v
que
u
v
oir
prit
.
c
hanger
est
v
b
la
(Le
se
otan
de
disp
harger
d'une
son
de
c
ondance
le
par
le
otan
passe
en
ote
le
oter
diéren
de
v
l'auditeur.
p
exp
s
désire
les
à
équiv
proto
ts,
Cette
p
1.2
t
v
de
son
phase
met
v
e
l'urne,
n'est
ctuer
SMS.
sto
ote
c
reçu
k
Cette
er
e
le
r
v
p
ote,
p
après
c
quelques
v
v
t
érications,
t
puis
son
v
ote,
a
même
générer
fois
u
v
n
t
autre
celui-ci
message
9
v
électeur,
V P B R
Vote
Vote Chiffré
Chiffré Modifié
Confirmation
Confirmation
Acceptation
Reçu eut
er
Ec
rat
hireur
é
p
ts
érier
lieu,
ensuite
u
tre
otes.
un
v
déroulée
soumission
A
de
la
ou
hireur,
au
l'ensem
v
Ainsi,
à
en
comme
sans
soit
l'auditeur
aucun
ble
résultat.
on
hi
t
que
Ainsi,
otan
ten
de
de
oie
n'a
nal.
sans
v
reçus
v
déc
la
v
otes
otes

s
d
des
de
de
érier
ort
son
ossible
jouter
aléatoire,
toutes
qu'un
o
à
l'auditeur
P
hashs
rés
qui
publie
été
il
l'urne
s'est
phase
otes
v
1.3
'auditeur
l'ordre
le
g
du
diére
çus
duran
et
déc
v
de
a
en
dans
en
le
des
ur
a
soit
du
t.
y
e
ec
tr
des
et
publication
les
hirés
hirés
i
p
à
otes
p
a
con
déc
hiré
soumission
l'auditeur
le
de
l'ordre
le
l'en
bien
en
v
tout
ou
p
e
rapp
foi
lien
conrmations
ordre
v
viter
y
des
à
our
l'ensem
dans
des
Remarque.
des
n'existe
otes
le
lui

t
et
soumis
ts,
ar
bien
duran
c
la
l'élection
de
insi,
des
Figure
otes.
v
l

p
à
comparer
han
con
n
u
es
générateur
hirés.
re
messages
sortie.
les
l'urne
t
v
v
qu'aucun
phase
ote
v
été
décompte
jouté
otes
supprimé
L'urne,
l'urne
l'urne
que
premier
géné
et
e
v
de
déc
ne
en
mis
les
couran
o
Le
sortie
hireur
er
ectue
l'ordre
son
ble
a
à
ail
v
en
v
oie
c
v
de
c
au
et
h
hireur

et
s
ui
l'auditeur.
hireur
en
v
ossession
v
u
fournir
ten
en
c
l'auditeur
l'urne,
la
résultats,
trée,
tre
a
l'ordre
déc
déc
l'ensem
est
ble
mesure
de
v
son
que
con
déc
ten
a
u,
fait
c'est-à-dire
tra
ces
ail
mêmes
supprimer
v
a
otes.
d
Le
v
générateur
Une
de
s
reçus
ces
v
eectuées,
a
conrme
en
10
et
A R B D
Votes Chiffrés
Hashs
Contenu
Votes Chiffrés
+ Votes Déchiffrés

Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.