Paper. What i write

Il lavoro affronta la verifica formale del protocollo di Single Sign-On (SSO) OpenID Connect 1.0, rilasciato come standard il 24 febbraio 2014. La premessa metodologica è che la progettazione di protocolli di autenticazione, pur apparentemente semplice, sia notoriamente soggetta a errori (vengono citati i casi di Kerberos v4 e del SAML SSO di Google Apps). L'obiettivo è verificare, mediante metodi formali automatici, se la formulazione minimale del protocollo soddisfi le proprietà di sicurezza attese.

L'analisi è condotta con AVISPA (Automated Validation of Internet Security Protocols and Applications), utilizzando il linguaggio di specifica HLPSL (High Level Protocol Specification Language), basato sui ruoli e sulla logica temporale (TLA di Lamport). Il modello dell'attaccante adottato è quello di Dolev-Yao (l'attaccante coincide con la rete). AVISPA integra quattro back-end, di cui il lavoro discute proprietà e limiti: OFMC, CL-AtSe, SATMC e TA4SP.

Tra i tre flussi di OpenID Connect (Authorization Code Flow, Implicit Flow, Hybrid Flow), il lavoro modella esclusivamente l'Authorization Code Flow. La formalizzazione parte da una notazione Alice-Bob con cinque attori (Relying Party, OpenID Provider, End-User, Token Endpoint, UserInfo Endpoint) e modella le sessioni TLS tramite chiavi simmetriche condivise (ROKey, RTKey, RUKey), oltre alla CSKey derivata dal client_secret. I goal verificati sono di tipo secrecy (sec_1 = Stat, sec_2 = Code, sec_3 = IdToken) e authentication (auth_1, auth_3).

Nella formulazione minimale (di default), i back-end OFMC, CL-AtSe e SATMC concordano nel risultato UNSAFE: viene rilevata una violazione della proprietà secrecy_of sec_2, ossia l'intercettazione del valore Code (l'Authorization Code) quando l'Intruder riveste il ruolo di OpenID Provider o di Token Endpoint. TA4SP restituisce esito INCONCLUSIVE (time-out), evidenziando un limite dello strumento.

La vulnerabilità viene rimossa cifrando/firmando i contenuti dei messaggi con la CSKey (derivata dal client_secret negoziato in fase di registrazione). Sulla specifica HLPSL corretta, OFMC, CL-AtSe e SATMC restituiscono esito SAFE (per un numero limitato di sessioni); TA4SP rimane inconclusivo.

Il protocollo, nella sua versione di base, presenta vulnerabilità limitate all'intercettazione di informazioni di sessione, eliminabili attivando funzionalità già previste dalla specifica (crittografia e firma JWT/JWS/JWE su TLS). Vengono inoltre richiamate le contromisure non catturabili da AVISPA (nonce contro i replay attack, state contro CSRF, AUD contro l'Access Token Redirect, ecc.) e si segnala l'esigenza di una maggiore espressività di HLPSL per modellare canali sicuri.