|
Jean Goubault-Larrecq |
G.I.E. Dyade, INRIA |
Méthodes formelles |
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 ? |
Spécification informelle du tri |
Spécifications formelles |
" l : int list, l' : int list · R (l, l') Þ tri (l, l') | (1) | |||
" l : int list · $ l' : int list · R (l, l') | (2) |
|
(3) | |||||||
|
(4) | |||||||
|
(5) | |||||||
|
(6) | |||||||
|
(7) | |||||||
|
(8) | |||||||
|
(9) | |||||||
|
(10) |
Est-ce la spécification que vous souhaitiez ? |
|
Comment s'assurer que sort3 est correct ? |
Autres méthodes formelles |
Applications aux protocoles cryptographiques |
Compromis (à l'heure actuelle) |
Le pionnier : la BAN (Burrows-Abadi-Needham) |
m | ::= | K | clés |
| | D | autres messages de base | |
| | mK | chiffrement | |
| | m, m | couples | |
| | ... |
Ambitions et défauts de la BAN |
Règles |
Exemple : Needham-Schroeder à clés symétriques |
1. | A ® S | : A, B, Na | ||||||||
2. | S ® A |
|
||||||||
3. | A ® B |
|
||||||||
4. | B ® A |
|
||||||||
5. | A ® B |
|
||||||||
Needham-Schroeder idéalisé |
1. | A ® S | : | |||||||||
2. | S ® A | : | |||||||||
|
|||||||||||
3. | A ® B | : | |||||||||
|
|||||||||||
4. | B ® A | : | |||||||||
|
|||||||||||
5. | A ® B | : | |||||||||
|
Needham-Schroeder analysé |
Le spi-calcul |
m | ::= | n | noms | |||||
| | x | variables | ||||||
| | 0 | |||||||
| | S (m) | données de base | ||||||
| |
|
chiffrement | ||||||
| | (m1, m2) | couples |
P | ::= |
|
émission | ||||||
| | m1 (x) . P | réception | |||||||
| | P1 | P2 | parallèle | |||||||
| | (n n) P | restriction | |||||||
| | !P | réplication | |||||||
| | [m1 is m2] P | test d'égalité | |||||||
| | 0 | nil | |||||||
| | let (x,y) = m in P | décomposition | |||||||
| | case m1 of 0:P S(x):Q | analyse de cas | |||||||
| |
|
déchiffrement |
Règles de calcul |
|
(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) |
Needham-Schroeder en spi-calcul |
|
|
|
Spécifications en spi-calcul |
Inst (F, G) | = | (n Kas) (n Kbs) | ||||||||
(A (F, Kas) | B (G, Kbs) | !S (Kas, Kbs)) | (15) | |||||||||
FM (x) | = |
|
(16) | |||||||
G (z) | = | cAB (z') . case z' of {y}z in H (y) | (17) |
Authentification |
Inst (F, G) | = | (n Kas) (n Kbs) | ||||||||
(A (F, Kas) | B (G, Kbs) | !S (Kas, Kbs)) | ||||||||||
FM (x) | = |
|
||||||||
GM (z) | = | cAB (z') . case z' of {y}z in H (M) | (18) |
L'approche de Dominique Bolignano |
Le rôle de A en tant qu'automate |
Modélisation du protocole |
Le prédicat known_in |
known_in (E È {m}, m) | |
known_in (E, m) Ù known_in (E, K) | known_in (E, mK) Ù known_in (E, K-1) |
Þ known_in (E, mK) | Þ known_in (E, m) |
known_in (E, m1) Ù known_in (E, m2) | known_in (E, (m1, m2)) |
Þ known_in (E, (m1, m2)) | Þ known_in (E, mi) |
Modélisation de la relation de transition |
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 ((sA, sB, sS, E), m, (s'A, s'B, s'S, E') = | |||||
sA = 1a(Na) Ù s'A = 2a(Na) Ù s'B = sB Ù s'S = sS | |||||
Ù E' = E È {m}Ù m = (idA, idB, Na) Ù ¬ known_in (E, Na) | |||||
P_reception_1 ((sA, sB, sS, E), m, (s'A, s'B, s'S, E') = | |||||
|
|||||
|
Modélisation du protocole |
Exec (s, s) P (s,l,m,s') Ù Exec (s',s'') Þ Exec (s,s'') |
¬ known_in (E0, Kas) ¬ known_in (E0, Kbs) |
Exec ((sA0, sB0, sS0, E0), (sAfin, sBfin, sSfin, Efin)) |
¬ known_in (Efin, Kab) |
¬ known_in (Efin, Kas) |
¬ known_in (Efin, Kbs) |
Quelques remarques |
This document was translated from LATEX by HEVEA.