Modelarea și verificarea protocoalelor de securitate cu ajutorul calculului Pi aplicat și ProVerif

Titlul original:

Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif

Conținutul cărții:

Verificarea protocoalelor de securitate a fost un domeniu de cercetare activ încă din anii 1990. Acest subiect este interesant din mai multe motive.

Protocoalele de securitate sunt omniprezente: ele sunt utilizate pentru comerțul electronic, rețelele fără fir, cărțile de credit, votul electronic, printre altele. Proiectarea protocoalelor de securitate este, în mod notoriu, predispusă la erori. Aceste erori pot avea, de asemenea, consecințe grave.

Prin urmare, verificarea sau demonstrarea formală a protocoalelor este deosebit de importantă.

Acest studiu se concentrează asupra verificării specificațiilor protocoalelor în modelul simbolic. Chiar dacă este destul de abstract, acest nivel de verificare este relevant în practică, deoarece permite descoperirea multor atacuri.

ProVerif este un verificator automat de protocoale simbolice. Acesta acceptă o gamă largă de primitive criptografice, definite prin reguli de rescriere sau prin ecuații. Acesta poate dovedi diverse proprietăți de securitate: secretul, autentificarea și echivalențele proceselor, pentru un spațiu de mesaje nelimitat și un număr nelimitat de sesiuni.

Acesta primește ca intrare o descriere a protocolului de verificat într-un dialect al calculului pi aplicat, o extensie a calculului pi cu criptografie. Acesta traduce automat această descriere a protocolului în clauze Horn și determină dacă proprietățile de securitate dorite sunt valabile prin rezolvarea acestor clauze. Acest studiu prezintă o imagine de ansamblu a cercetării privind ProVerif și este cel mai cuprinzător text disponibil pe această temă.