Méthodes formelles

et protocoles cryptographiques

Jean Goubault-Larrecq

G.I.E. Dyade, INRIA

Méthodes formelles;
Application aux protocoles cryptographiques.

Méthodes formelles

But : assurer qu'un programme est correct.

Idée de base : vérifier que le programme satisfait une propriété mathématique (appelée spécification).

Un exemple-jouet, le tri par fusion (en ML)

Un exemple-jouet, le tri par fusion (en C)

Spécification: qu'est-ce qu'un tri ?

Intuitivement, les deux programmes précédents font la même chose (trier), mais il y a des différences : lesquelles ? (regardez bien, le 2ème est faux...corrigez-le.)

À l'opposé, qu'y a-t-il de commun entre ces deux programmes ? Et avec le suivant ?

Spécification informelle du tri

``Un tri prend une liste l en entrée et retourne la liste des mêmes éléments en ordre croissant.''

Les comportements suivants de ma fonction sort3 sont-ils acceptables, selon vous ?

sort3 [1,2,3,2] = [1,2,3];
sort3 [1,2,3,2] = [1,2,2,3];
sort3 [1,2,3] = [1,2,2,3];
sort3 [1,2,3,2] retourne parfois [1,2,3], parfois [1,2,2,3];
sort3 [1,2,3] ne termine pas.

Spécifications formelles

Par exemple, on modélise le fait que sort3 (l) retourne l' par une relation binaire R (l, l'), on veut donc vérifier :

			" l : `int list`, l' : `int list` · R (l, l') Þ tri (l, l')	(1)
			" l : `int list` · $ l' : `int list` · R (l, l')	(2)

sous les hypothèses (définitions, ici) :

" l : int list, l' : int list ·

tri (l, l') Û (memes_elements (l, l') Ù ordre_croissant (l'))

(3)

" l : int list, l' : int list ·

memes_elements (l, l') Û sous_liste (l, l') Ù sous_liste (l', l)

(4)

" l : int list, l' : int list ·

sous_liste (l, l') Û (" i : N ·

0 £ i Ù i < len (l) Þ

$ j : N · 0 £ j Ù j < len (l') Ù sub (l, i) = sub (l', j))

(5)

" l : int list ·

ordre_croissant (l) Û (" i : N, j : N ·

0 £ i Ù i£ j Ù j < len (l) Þ sub (l, i) £ sub (l, j)

(6)

len ([]) = 0

(7)

" l : int list, x : int · len (x::l) = len (l) + 1

(8)

" l : int list, x : int · sub (x::l, 0) = x

(9)

" l : int list, x : int, i : int · sub (x :: l, i+1) = sub (l, i)

(10)

Est-ce la spécification que vous souhaitiez ?

Une autre (en logique d'ordre 2); remplacer (4) et (5) par :

" l : int list, l' : int list ·

memes_elements (l, l') Û $ p : N ® N ·

(" j : N · $! i : N · p (i) = j) Ù

(" i : N · 0£ i Ù i < len (l) Þ

0£ p (i) Ù p (i) < len (l') Ù sub (l', p (i)) = sub (l, i))

Comment s'assurer que sort3 est correct ?

Dépend du niveau de confiance que l'on veut atteindre :

Test (indispensable, mais ne donne que peu de garanties);
Relecture du code (si possible par un autre);
Écriture de la spécification (détecte les ambiguïtés);
Preuve de correction informelle (à la main);
Preuve automatique de programmes (infaisable);
Dérivation automatique de propriétés par interprétation abstraite;
Preuve formelle (d'une idéalisation suffisamment poussée), c'est-à-dire mécanisée.

Autres méthodes formelles

Méthodes orientées modèles : VDM, Z, B, Raise, etc.
Méthodes d'états finis : model-checking de formules en logique temporelle (spécifications) sur des automates finis (les programmes).
Extraction de programmes; en logique intuitionniste, toute preuve de " x· $ y · P (x,y) est un programme calculant y en fonction de x : Coq, NuPrl, LF, etc.
Algèbres de processus (pour programmes parallèles), notions d'équivalence opérationnelle approchées par des bisimulations: CSP, CCS, p-calcul, etc.

Applications aux protocoles cryptographiques

Logiques modales la BAN;
Algèbres de processus le spi-calcul;
Les méthodes orientées modèle l'approche de D. Bolignano.

Compromis (à l'heure actuelle)

Le pionnier : la BAN (Burrows-Abadi-Needham)

Modèle très simple de données :

m	::=	K	clés
	\|	D	autres messages de base
	\|	m_K	chiffrement
	\|	m, m	couples
	\|	...

Bizarrerie : messages º formules. Logique modale avec opérateurs ``croit'', ``voit'', ``a dit'', ``a juridiction sur'', ``est frais'', ``est un secret entre'', etc.

Ambitions et défauts de la BAN

Ambition modeste : trouver des bugs de nature logique, i.e. indépendants de la qualité des algorithmes cryptographiques utilisés.
Résultat surprenant : de nombreuses attaques sont de nature logique.
Défauts : ne permet pas de prouver qu'un protocole est correct; mauvaise notion de fraîcheur; faiblesse des postulats permettant de conclure qu'une donnée est secrète; nécessité d'une étape d'idéalisation; etc.

Règles

``Si P croit P «^K Q, et P voit X_K, alors P croit que Q a dit X.''

``Si P croit Y secret entre P et Q, et P voit X, Y, alors P croit que Q a dit X.''

``Si P croit X frais, et que Q a dit X, alors P croit que Q croit X.''

``P croit X,Y ssi P croit X et P croit Y.''

``Si P croit que Q a dit X,Y, alors P croit que Q a dit X (resp. Y).''

``Si P voit X,Y, alors P voit X (resp. Y).''

``Si P croit P «^K Q et P voit X_K, alors P voit X.''

``Si P croit X (resp. Y) frais, alors P croit X, Y frais.''

Exemple : Needham-Schroeder à clés symétriques

A ® S

: A, B, N_a

S ® A

: {N_a, B, K_ab, {K_ab, A}

K_bs

}

K_as

A ® B

: {K_ab, A}

K_bs

B ® A

: {N_b}

K_ab

A ® B

: {N_b-1}

K_ab

Needham-Schroeder idéalisé

A ® S

S ® A

{N_a, A «^K_ab B, A «^K_ab B frais

, {A «^K_ab B}

K_bs

}

K_as

A ® B

{A «^K_ab B}

K_bs

B ® A

{N_b, A «^K_ab B }

K_ab

A ® B

{N_b, A «^K_ab B }

K_ab

Needham-Schroeder analysé

Sous les hypothèses :

``A croit A «^K_as S, B croit B «^K_as S.''

``S croit A «^K_ab B.''

``A croit que S a juridiction sur A «^K B, " K.''

...

``B croit A «^K B frais, " K.'' (*)

On déduit ``B (resp. A, A croit que B, B croit que A) croit A «^K_ab B.'' (Sans (*), seulement ``B croit que S a dit A «^K_ab B.'')

Le spi-calcul

Termes :

::=

noms

variables

S (m)

données de base

{m₁}

m₂

chiffrement

(m₁, m₂)

couples

Processus :

::=

m₁

á m₂ ñ . P

émission

m₁ (x) . P

réception

P₁ | P₂

parallèle

(n n) P

restriction

réplication

[m₁ is m₂] P

test d'égalité

nil

let (x,y) = m in P

décomposition

case m₁ of 0:P S(x):Q

analyse de cas

case m₁ of {x}

m₂

in P

déchiffrement

Pas de logique, ce n'est qu'un langage de programmation.

Règles de calcul

(

á m' ñ . P) | (m (x) . Q) ® P | (Q[m'/x])

(11)

case 0 of 0:P S (x):Q ® P

(12)

case S (m) of 0:P S (x):Q ® Q [m/x]

(13)

case {m}_m' of {x}_m' in P ® P[m/x]

(14)

etc.

Needham-Schroeder en spi-calcul

A (F, K_as) =

/* 1. A ® S */

(n N_a)

_AS á id_A, id_B, N_a ñ .

/* 2. */

c_SA (x) .

case x of {x'}

K_as

let (x

N_a

, x_B, x_K, x'')

=x' in

N_a

is N_a] [x_B is id_B]

/* 3. A ® B */

_AB á x'' ñ .

/* 4. */

c_BA (x''') .

case x''' of {x

N_b

}_K in

/* 5. A ® B */

_AB á {x

N_b

-1}_K ñ . F (K)

B (G, K_bs) =

/* 3. */

c_AB (z) .

case z of {z'}

K_bs

let (K, z_A) = z' in

[z_A is id_A]

/* 4. B ® A */

(n N_b)

_BA á {N_b}_K ñ .

/* 5. */

c_AB (z'') .

case z'' of {z'''}_K in

[z''' is N_b-1] G (K)

S (K_as, K_bs) =

/* 1. */

c_AS (y_A, y_B, y

N_a

) .

/* 2. S® A */

(n K_ab)

_SA á {y

N_a

, y_B, K_ab,

{K_ab, y_A}

K_bs

}

K_as

ñ .

Spécifications en spi-calcul

Inst (F, G)

(n K_as) (n K_bs)

(A (F, K_as) | B (G, K_bs) | !S (K_as, K_bs))

(15)

F_M (x)

_AB á {M}_x ñ .

(16)

G (z)

c_AB (z') . case z' of {y}_z in H (y)

(17)

Équivalence observationnelle : P Q ssi P et Q sont indistingables dans tout contexte.

K garantit une communication secrète ssi, pour tout H, pour tous M, M' tels que H(M) H(M'), Inst (F_M, G) Inst (F_M', G).

Authentification

Inst (F, G)

(n K_as) (n K_bs)

(A (F, K_as) | B (G, K_bs) | !S (K_as, K_bs))

F_M (x)

_AB á {M}_x ñ .

G_M (z)

c_AB (z') . case z' of {y}_z in H (M)

(18)

K garantit l'authenticité des messages ssi, pour tout H, pour tout M, Inst (F_M, G) Inst (F_M, G_M).

L'approche de Dominique Bolignano

Attitude inverse du spi-calcul : on n'a plus que des formules (en logique du premier ordre). La sémantique du programme est décrite sous forme d'un ensemble de formules, exécutables par Prolog.

L'exécution du protocole est un automate infini.

La méthode est paramétrable par divers modèles de sécurités (des axiomes).

Dérivation de preuves formelles (à l'heure actuelle en Coq).

Le rôle de A en tant qu'automate

Modélisation du protocole

Le système (A | B | S | I, où I est l'intrus) est modélisé comme un automate produit; chaque état s est un quadruplet (s_A, s_B, s_S, E).

Pour ce qui est des propriétés de sécurité, on peut supposer que l'on est dans le pire des cas : tous les principaux parlent à l'intrus, reçoivent leurs messages de l'intrus. À tout instant, l'intrus possède un ensemble E de messages (espionnés sur les canaux), et ne peut fabriquer que des messages m tels que known_in (E, m).

Le prédicat known_in

...est défini inductivement par :

known_in (E È {m}, m)

known_in (E, m) Ù known_in (E, K)	known_in (E, m_K) Ù known_in (E, K^-1)
Þ known_in (E, m_K)	Þ known_in (E, m)

known_in (E, m₁) Ù known_in (E, m₂)	known_in (E, (m₁, m₂))
Þ known_in (E, (m₁, m₂))	Þ known_in (E, m_i)

Modélisation de la relation de transition

Écriture d'un prédicat P (état-avant, transition, message, état-après).

P (s, l, m, s') =	(l=émission-1. Ù P_emission_1 (s, m, s'))
	Ú (l=réception-1. Ù P_reception_1 (s, m, s'))
	Ú ...

P_emission_1 ((s_A, s_B, s_S, E), m, (s'_A, s'_B, s'_S, E') =

s_A = 1a(N_a) Ù s'_A = 2a(N_a) Ù s'_B = s_B Ù s'_S = s_S

Ù E' = E È {m}Ù m = (id_A, id_B, N_a) Ù ¬ known_in (E, N_a)

P_reception_1 ((s_A, s_B, s_S, E), m, (s'_A, s'_B, s'_S, E') =

s_S = 1s () Ù s'_S = 2s (x_A, x_B, x

N_a

) Ù s'_A = s_A Ù s'_B = s_B

Ù E' = E Ù m = (x_A, x_B, x

N_a

) Ù known_in (E, m)

Modélisation du protocole

Exécution :

Exec (s, s) P (s,l,m,s') Ù Exec (s',s'') Þ Exec (s,s'')

Hypothèses de départ :

¬ known_in (E₀, K_as) ¬ known_in (E₀, K_bs)

Exec ((s_A0, s_B0, s_S0, E₀), (s_Afin, s_Bfin, s_Sfin, E_fin))

Montrer :

¬ known_in (E_fin, K_ab)

¬ known_in (E_fin, K_as)

¬ known_in (E_fin, K_bs)

Quelques remarques

Souple : on peut changer le modèle de sécurité (ici, pour simplifier, on avait confiance en A, B et S, et S était en mono-session).

S'étend à de gros protocoles cryptographiques, y compris de commerce électronique.

L'exécution Prolog retourne soit ``non'', soit une attaque. Dans le premier cas, la trace Prolog fournit l'argument de preuve.

This document was translated from L^AT_EX by H^EV^EA.