L5. Modelarea si validarea protocolului cu chei publice Needham-Schroeder

Descrierea protocolului

http://www.lsv.ens-cachan.fr/Software/spore/nspk.html

A,B,S : 			Principal
Na,Nb : 			Nonce
KPa,KPb,KPs,KSa,KSb,KSs : 	Cheie
KPa,KSa : 			pereche de chei
KPb,KSb : 			pereche de chei
KPs,KSs : 			pereche de chei

1. A -> S : A,B
2. S -> A : {KPb, B}KSs
3. A -> B : {Na, A}KPb
4. B -> S : B,A
5. S -> B : {KPa, A}KSs
6. B -> A : {Na, Nb}KPa
7. A -> B : {Nb}KP

Entitatile implicate in protocol sunt cei doi agenti intre care se face autentificarea, A(lice) si B(ob), respectiv server-ul S, al carui rol este acela al distributiei cheilor publice. In descrierea protocolului, KS reprezinta cheile secrete ale entitatilor, iar KP, cheile publice. In comunicatia dintre A si B, cheile publice sunt utilizate in criptarea mesajelor, astfel incât doar destinatarii acestora sa le poata decripta cu ajutorul cheilor secrete. In cadrul procesului de distributie a cheilor, mesajele sunt criptate cu cheia secreta a lui S, iar decriptarea se face cu ajutorul cheii publice. Pentru ca protocolul sa poata functiona, se presupune ca toate entitatile implicate cunosc deja cheia publica a lui S, in momentul in care acesta este interogat.
Obiectivul protocolului este obtinerea unei chei secrete, cunoscute doar de agentii A si B.
Operatia de criptare este reprezentata prin { mesaj } K , unde K este cheia folosita la criptare, iar mesaj, informatia criptata. Daca mesajele au mai multe câmpuri, se presupune ca destinatarul le poate distinge la decriptare. Numerele Na si Nb poarta numele de nonce (number used once) in jargon criptografic, indicând faptul ca pot fi utilizate o singura data (intr-o singura executie a protocolului). Acestea sunt utilizate pentru crearea cheii de sesiune pentru comunicatia ulterioara dintre A si B.
Modelarea protocolului va porni de la ipoteza ca algoritmii de criptare utilizati sunt fiabili, iar mesajele criptate pot fi decriptate doar de posesorii cheilor corespunzatoare. In aceste conditii, daca nici o alta entitate nu cunoaste cheia secreta a lui S, putem spune ca etapa distributiei cheilor publice se desfasoara in conditii de securitate (cheia publica a fiecarui agent este insotita de identificatorul acestuia, in cadrul sectiunii criptate a mesajului).
Putem face prima simplificare a modelului: presupunem ca A si B cunosc deja toate cheile publice necesare comunicatiei. Nu mai este necesara includerea in model a entitatii Server. De asemeni, deoarece din exterior sunt cunoscute doar cheile publice, care pot fi utilizate doar pentru criptare, putem simplifica si notatiile cheilor din KPa si KPb in Ka, respectiv Kb. Comunicatia se va rezuma la urmatoarele mesaje:

1. A -> B : {A, Na}Kb
2. B -> A : {Na, Nb}Ka
3. A -> B : {Nb}Kb

Protocolul va functiona astfel:

1. Alice genereaza numarul aleator Na si transmite mesajul {A, Na}_Kb catre Bob. Primul câmp al mesajului reprezinta identitatea initiatorului comunicatiei, iar al doilea, jumatate din secretul comun.
2. Dupa receptia primului mesaj, B creaza si el un numar aleator, Nb, pe care-l include in mesajul: {Na, Nb}_Ka. Prezenta primului nonce in mesaj, pe care l-ar fi putut decripta doar B, are rolul de a-l convinge pe A in privinta autenticitatii mesajului. A va accepta perechea (Na, Nb) ca fiind secretul comun.
3. Alice raspunde cu mesajul {Nb}_Kb, confirmându-i astfel lui B autenticitatea sesiunii. B va accepta si el perechea (Na, Nb) ca fiind secretul comun.

Cheia de sesiune (Na, Nb) poate fi utilizata in cadrul unui interval limitat de timp.
Se presupune ca toate mesajele sunt transmise pe un mediu de comunicatie nesigur (nesecurizat). Un atacator ar putea obtine astfel informatii utile pentru compromiterea schemei de securitate.
Vom utiliza modelul Dolev-Yao al atacatorului, unde un tert poate intercepta, stoca sau sintetiza orice mesaj. Acesta poate participa si in executii partiale ale protocolului, dar nu poate decripta decât mesajele criptate cu cheia sa publica.
Inainte de a trece la modelarea sistemului, se mai fac doua ipoteze simplificatoare:

• reteaua va include doar doi agenti, A si B (ulterior, va fi adaugat si al treilea – intrusul)
• agentii A si B participa fiecare intr-o singura executie a protocolului.

In aceste conditii, un agent poate declansa procesul de autentificare, iar celalalt poate doar sa accepte aceasta initiativa. In consecinta, fiecare agent va crea un singur nonce si va participa intr-o singura sesiune.
Se presupune ca agentii A si B sunt onesti.
Chiar daca protocolul este unul de mici dimensiuni, simplificarile sunt tipice pentru pentru analiza prin model-checking: modelele trebuie sa aiba un numar finit (cât mai mic) de stari, complexitatea analizei depinzând exponential de dimensiunea modelelor. Datorita simplificarilor este uneori posibil ca unele erori sau vulnerabilitati (daca discutam despre protocoale de securitate) precum cele care apar in cazul mai multor executii ale protocolului sa nu fie detectate. De aceea, atunci când nu se detecteaza defecte in cadrul modelului curent utilizat, se poate trece la verificarea unor modele mai complexe.
Intr-o prima faza, vom modela doar entitatile A si B si vom verifica in primul rând corectitudinea codului. De asemeni, vom simula executia protocolului, pentru a avea o baza de comparatie in cazul in care vor fi identificate vulnerabilitati.
Pentru a usura interpretarea modelului (de catre cititor), se definesc nume(constante) simbolice pentru toate informatiile implicate in executia protocolului:

mtype = {   ok, err,
	    msg1, msg2, msg3,
	    kA, kB, kI,
	    A, B, I,
	    NA, NB, NI
	}

Primele doua se refera la starea entitatii de protocol. Pentru fiecare agent se defineste câte o variabila de stare, care se initializeaza cu err. Atunci când agentul ia decizia ca in urma executiei s-a negociat o cheie de sesiune valida, isi va actualiza variabila stare ca fiind ok. Variabila nu este implicata in deciziile luate de-a lungul executiei protocolului, dar poate fi utilizata pentru testarea starii curente a protocolului. Ulterior, aceste variabile vor fi utilizate in cadrul procesului de verificare a protocolului.
kA si kB sunt cheile publice ale celor doua entitati de protocol, iar A si B, identitatile acestora. De asemeni, pentru verificarea protocolului este necesara cunoasterea partenerului fiecarui agent. Chiar daca A si B stabilesc fiecare câte o cheie de sesiune, aceste chei pot fi valabile intre cei doi agenti, sau intre agenti si un tert. Aceste definitii sunt incluse in instructiunile:

mtype partnerA
mtype statusA = err
mtype partnerB
mtype statusB = err

Pentru a mima comunicatia securizata si criptarea informatiilor, se creaza un tip de date complex:

typedef Crypt { mtype key, data1, data2 }

, unde key reprezinta cheia de criptare a mesajului, dar data1, data2, câmpurile acestuia. Decriptarea mesajelor din acest model va fi echivalenta cu verificarea potrivirii cheii incluse in mesaj cu cheia privata a fiecarui agent. Copierea dintr-o singura operatie a tuturor câmpurilor unui mesaj criptat catre alt mesaj criptat este imposibila in Promela. Totusi, deoarece este permisa definirea de functii macro, pentru simplificarea modelului, se definesc functiile crypt(m, a, b, c) si copy(a, b):

#define crypt(m, a, b, c) m.key=a;m.data1=b;m.data2=c
#define copy(a, b) b.key = a.key; b.data1 = a.data1; b.data2 = a.data2

Formatul mesajului va fi urmatorul:

/---------------------------------\
| tip_msg | destinatar | continut |
\---------------------------------/

Tipul mesajului poate fi oricare dintre cele trei definite mai sus (msg1÷3), iar pe post de destinatie vor fi utilizate chiar identitatile agentilor. Câmpul continut corespunde mesajului criptat. Deoarece prin protocol nu se presupune transmisia mai multor mesaje simultan, canalul de comunicatie poate fi modelat ca având buffer de dimensiune zero:

chan network = [0] of { mtype,  	/* msg ID */
			mtype,  	/* destinatie */
			Crypt }

Pentru verificarea starii protocolului s-au mai definit o serie de macro-uri(propozitii atomice):

#define auth (statusA==ok && statusB==ok)
#define pAB (partnerA==B)
#define pBA (partnerB==A)

Prima expresie poate fi utilizata pentru verificarea faptului ca ambele entitati de protocol s-au autentificat, iar celelalte doua permit verificarea ipotezei ca partenerul de comunicatie al lui A va fi B si viceversa.
Datorita simplificarilor facute, comportamentele celor doi agenti vor fi complementare. Cea mai importanta diferenta este ca A il alege pe B ca partener, in timp ce lui B i se cere sa comunice cu A.
Protocolul trebuie sa functioneze doar atunci când câmpurile mesajelor receptionate de cei doi agenti sunt corecte, caz in care protocolul trebuie sa ajunga la finalul executiei. Altfel, este suficienta blocarea executiei entitatilor de protocol pentru a semnala detectia unui mesaj incorect.
Pe baza ipotezelor anterior prezentate, protocolul se poate modela astfel:

mtype = {   ok, err,
	    msg1, msg2, msg3,
	    kA, kB,
	    A, B,
	    NA, NB
	}
typedef Crypt { mtype key, data1, data2 }
chan network = [0] of { mtype,  	/* msg ID */
			mtype,  	/* destinatie */
			Crypt }

mtype partnerA
mtype statusA = err
mtype partnerB
mtype statusB = err


#define crypt(m, a, b, c) m.key=a;m.data1=b;m.data2=c
#define copy(a, b) b.key = a.key; b.data1 = a.data1; b.data2 = a.data2


#define auth (statusA==ok && statusB==ok)
#define pAB (partnerA==B)
#define pBA (partnerB==A)


active proctype Alice() {
    mtype pkey, pnonce;
    Crypt data, msg;
    
    partnerA = B; pkey = kB;
    
    crypt(msg, pkey, A, NA);
    network ! msg1 (partnerA, msg);
    
    network?(msg2, A, data);
    (data.key == kA) && (data.data1 == NA);
    pnonce = data.data2;
    
    network ! msg3(partnerA, pkey, pnonce, 0);
    statusA = ok;
}


active proctype Bob() {
    mtype pkey, pnonce;
    Crypt data, msg;
    
    network?(msg1, B, data);
    (data.key == kB);
    partnerB = data.data1;
    pnonce = data.data2;
    
    (partnerB == A) -> pkey = kA;
    
    crypt(msg, pkey, pnonce, NB);
    network ! msg2 (partnerB, msg);
    
    network ? msg3 (B, kB, NB, _);
    statusB = ok;
}

Rezultatul simularii este urmatorul:

$ spin -s -r ns.pml 
  6:	proc  0 (Alice) ns.pml:34 Sent msg1,B,kB,A,NA	-> queue 1 (network)
  6:	proc  1 (Bob) ns.pml:49 Recv msg1,B,kB,A,NA	<- queue 1 (network)
 15:	proc  1 (Bob) ns.pml:57 Sent msg2,A,kA,NA,NB	-> queue 1 (network)
 15:	proc  0 (Alice) ns.pml:36 Recv msg2,A,kA,NA,NB	<- queue 1 (network)
 18:	proc  0 (Alice) ns.pml:40 Sent msg3,B,kB,NB,0	-> queue 1 (network)
 18:	proc  1 (Bob) ns.pml:59 Recv msg3,B,kB,NB,0	<- queue 1 (network)
2 processes created

Spunem ca protocolul si-a incheiat in mod corect executia daca starile ambelor entitati indica autentificarea. Deci, conditia ca autentificarea sa se fi facut cu succes este (statusA==ok && statusB==ok), echivalent cu propozitia atomica auth anterior definita. Dorim sa aflam in ce conditii se ajunge la concluzia ca autentificarea s-a incheiat cu succes. Deoarece spin verifica validitatea acestei propozitii in fiecare din starile automatului extins creat, trebuie sa punem conditia ca autentificarea sa se faca eventual. Ca sa detecteze acest tip de evenimente, expresia trebuie negata. Expresia LTL corespunzatoare (adaugata sa sfarsitul modelului) va fi

ltl p0 { ! <> auth}

Rezultatul verificarii va fi:

$ spin -a ns.pml 
ltl p0: ! (<> (((statusA==ok)) && ((statusB==ok))))
$ gcc -DSAFETY -o pan pan.c
$ ./pan -c0 -e
warning: never claim + accept labels requires -a flag to fully verify
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
pan:1: end state in claim reached (at depth 34)
pan: wrote ns.pml1.trail
pan: wrote ns.pml2.trail
pan: wrote ns.pml3.trail
pan: wrote ns.pml4.trail

(Spin Version 6.0.1 -- 16 December 2010)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (p0)
	assertion violations	+ (if within scope of claim)
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	- (disabled by never claim)

State-vector 48 byte, depth reached 35, errors: 4
       22 states, stored
        5 states, matched
       27 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

    2.501	memory usage (Mbyte)

unreached in proctype Alice
	(0 of 12 states)
unreached in proctype Bob
	(0 of 13 states)
unreached in claim p0
	(0 of 8 states)

pan: elapsed time 0.02 seconds
pan: rate      1100 states/second

Comparand cele 4 fisiere trail rezultate se va ajunge la concluzia ca a fost identificat acelasi rezultat.
Automatul Büchi corespunzator expresiei verificate (fisierul _spin_nvr.tmp) este:

never p0 {    /* !(! (<> (((statusA==ok)) && ((statusB==ok))))) */
T0_init:
	if
	:: ((((statusA==ok)) && ((statusB==ok)))) -> goto accept_all
	:: (1) -> goto T0_init
	fi;
accept_all:
	skip
}

SPIN permite reprezentarea masinilor cu stari si in format grafic:

$ ./pan -D | dot -Tps > fsm.ps

Expresia care sta la baza acestui automat nu corespunde unei erori, dar poate fi folosita pentru evidentierea situatiilor in care procesul de autentificare se incheie cu succes.
Verificatorul functioneaza pe principiul constructiei intregului spatiu de stari corespunzator modelului si a verificarii fiecarei cai de executie cu ajutorul automatului Büchi. Pentru fiecare tranzitie din interiorul sistemului de tranzitii astfel construit, este executata o instructiune din cadrul automatului Büchi. Daca se ajunge in starea finala a automatului Büchi, atunci a fost detectata o incalcare a clauzei temporale si se salveaza intr-un fisier traseul parcurs de model pâna la invalidarea expresiei LTL (daca nu s-a specificat altfel de catre utilizator). Se trece apoi la continuarea verificarii, daca nu a fost detectat deja numarul de erori specificat de utilizator (prin argumentul -cN, unde N este numarul erorii la care se va opri verificarea).
MSC-ul corespunzator situatiei curente (generat de iSPIN) este:

Modelarea entitatii intrus

Spre deosebire de entitatile descrise anterior, atacatorul nu poate fi modelat prin intermediul vreunui protocol. Deoarece obiectivul acestei lucrari este identificarea automata a vulnerabilitatilor protocoalelor de securitate, pentru intrus va fi utilizat un model nedeterminist: vor fi descrise doar actiunile posibile in fiecare stare, iar SPIN va construi toate tranzitiile posibile.
Atacatorul poate fie sa intercepteze un mesaj (sau sa primeasca un mesaj care-i este destinat), fie sa construiasca un mesaj cu ajutorul informatiilor disponibile.
Spre deosebire de A si B, intrusul (I) poate primi orice mesaj, indiferent de destinatia acestuia. Daca mesajul ii este destinat altcuiva, poate lua decizia de a transmite mai departe mesajul, pentru a permite executia in continuare a protocolului, sau poate bloca mesajul. De asemeni, exista posibilitatea de a memora mesajele pe care nu le poate decripta.
Pentru simplitate, intrusul poate lua decizia memorarii câte unui mesaj corespunzator fiecarui tip. Deci pot fi memorate trei mesaje. De asemeni, daca poate decripta mesajele primite (doar daca acestea au fost criptate cu ajutorul cheii sale private), poate extrage si valorile Na sau Nb.
Cu ajutorul informatiilor obtinute, atacatorul poate genera noi mesaje arbitrare pe care le poate transmite ulterior si celorlalti agenti. O mare parte a acestor mesaje vor fi incorecte, fapt pe care agentii onesti il vor detecta, ceea ce va duce la un numar mare de blocaje (deadlocks). Deoarece in obiectivul acestei lucrari este verificarea securitatii protocoalelor, in cautarea posibilelor vulnerabilitati ale protocoalelor putem ignora complet aceste blocaje.
Tabelul urmator prezinta informatiile pe care le poate extrage atacatorul din mesajele interceptate:

Interceptat	Memorat
{A, NA }kI	NA
{NA , _ }kI	NA
{ NA }kI	NA
{B, NB }kI	NB
{NB , _ }kI	NB
{ NB }kI	NB
{ _ } kA	{ _ } kA
{ _ } kB	{ _ } kB

Se vor utiliza aceleasi entitati de protocol pentru agentii onesti A si B, dar se implementeaza si al treilea agent, I(ntruder – atacatorul).
Deoarece modelul atacatorului este mult mai complex, iar dimensiunea masinii cu stari construite de verificator creste aproape (datorita reducerii partiale a ordinului) exponential cu dimensiunea masinii cu stari a intrusului, este posibila situatia in care simularea va esua din lipsa de memorie.
Modelul complet este inclus in fisierul: atac.pml
Inca de la inceputul modelarii intrusului, se pleaca de la ipoteza ca si cheia sa publica este cunoscuta si poate fi distribuita de server.

Validarea protocolului

Obiectivul protocolului este acela de a asigura autentificarea intre entitati, garantând si confidentialitatea cheii de sesiune. Asadar, daca daca A si B au incheiat cu succes executia protocolului, atunci A trebuie sa creada ca partenerul sau este B si viceversa. Mai important, atacatorul nu trebuie sa cunoasca nonce-urile emise de cei doi agenti onesti, decât atunci când ii sunt adresate lui. Aceste proprietati pot fi exprimate astfel:

P1: [] (statusA == ok && statusB == ok  => 
		( partnerA == B <=> partnerB == A ) )
P2: [] (statusA == ok && partnerA == B => !knows_nonceA)
P3: [] (statusB == ok && partnerB == A => !knows_nonceB)

Cea mai importanta proprietate se bazeaza pe obiectivul insusi al protocolului. La incheierea executiei protocolului, daca nu exista nici o vulnerabilitate, trebuie sa existe doua posibilitati: ori autentificarea s-a incheiat intre cei doi agenti onesti, ori separat intre perechile (agent B, instrus) si (agent A, instrus). In a doua varianta, se presupune ca atât A, cât si B stiu ca s-au autentificat cu partenerul I. Proprietatile 2 si 3 vor fi utilizate pentru a verifica ipoteza ca atunci cand un agent onest crede ca are un partener altul decât I, atacatorul nu trebuie sa cunoasca nonce-ul generat de acesta.