FORMALIZZAZIONE DEL PROTOCOLLO SAML SSO …marino.miculan/data/labs/SAMLinHLPSL.… · SAML si basa...

UNIVERSITA DEGLI STUDI DI UDINE

Facolta di Scienze Matematiche, Fisiche e Naturali

Corso di Laurea Specialistica in Informatica

Progetto di Laboratorio Avanzato di Reti di Calcolatori eSicurezza

FORMALIZZAZIONE DEL PROTOCOLLOSAML SSO IMPLEMENTATO DA GOOGLE

IN HLPSL

Docente: Studente:Prof. MARINO MICULAN RICCARDO DI STASI

(MAT. 88548)

ANNO ACCADEMICO 2007-2008

Indice

1 Introduzione 1

2 SAML SSO 32.1 Il protocollo SAML SSO . . . . . . . . . . . . . . . . . . . . . . 32.2 Implementazione Google di SAML ed il relativo attacco . . . . . 6

3 Formalizzazione di SAML in HLPSL 113.1 Formalizzazione con chiavi simmetriche . . . . . . . . . . . . . . 113.2 Formalizzazione con chiavi asimmetriche . . . . . . . . . . . . . 15

4 Risultati ottenuti con Avispa 174.1 Risultati della versione a chiavi simmetriche . . . . . . . . . . . 174.2 Risultati della versione a chiavi asimmetriche . . . . . . . . . . . 19

5 L’implementazione corretta di Google 235.1 La nuova versione di SAML . . . . . . . . . . . . . . . . . . . . 23

6 Conclusione 25

A Codice sorgente prodotto 27A.1 Sorgente della versione errata a chiavi simmetriche . . . . . . . . 27A.2 Sorgente della versione errata a chiavi asimmetriche . . . . . . . 29A.3 Sorgente della versione corretta a chiavi simmetriche . . . . . . 32A.4 Sorgente della versione corretta a chiavi asimmetriche . . . . . . 34

B Output di Avispa 37B.1 Output della versione errata a chiavi simmetriche . . . . . . . . 37

B.1.1 Output di ofmc . . . . . . . . . . . . . . . . . . . . . . . 37B.1.2 Output di satmc . . . . . . . . . . . . . . . . . . . . . . . 38B.1.3 Output di cl-atse . . . . . . . . . . . . . . . . . . . . . . 39

B.2 Output della versione errata a chiavi asimmetriche . . . . . . . . 41B.2.1 Output di ofmc . . . . . . . . . . . . . . . . . . . . . . . 41

iii

iv INDICE

B.2.2 Output di satmc . . . . . . . . . . . . . . . . . . . . . . . 42B.2.3 Output di cl-atse . . . . . . . . . . . . . . . . . . . . . . 43

B.3 Output della versione corretta a chiavi simmetriche . . . . . . . 45B.3.1 Output di ofmc . . . . . . . . . . . . . . . . . . . . . . . 45B.3.2 Output di satmc . . . . . . . . . . . . . . . . . . . . . . . 45B.3.3 Output di cl-atse . . . . . . . . . . . . . . . . . . . . . . 46

B.4 Output della versione corretta a chiavi asimmetriche . . . . . . 47B.4.1 Output di ofmc . . . . . . . . . . . . . . . . . . . . . . . 47B.4.2 Output di satmc . . . . . . . . . . . . . . . . . . . . . . . 47B.4.3 Output di cl-atse . . . . . . . . . . . . . . . . . . . . . . 48

Bibliografia 51

Capitolo 1

Introduzione

Sempre piu spesso, le aziende che forniscono servizi su Internet mettono adisposizione dei loro clienti collezioni di applicazioni, in modo da cercare diesaudire tutte le esigenze informatiche di quest’ultimi. Con l’aumentare dellefunzionalita erogate da un singolo operatore, non e piu pensabile gestire leautenticazioni in modo separato per ogni applicazione, in quanto cio richiede-rebbe sia la memorizzazione di piu coppie username-password per un singoloutente, sia che ogni persona si ricordi delle credenziali di accesso usate perogni singolo servizio. Una soluzione a questo problema e quella offerta dall’usodi SAML, un’applicazione XML che permette di esprimere delle asserzioni disicurezza. SAML mette a disposizione diverse funzionalita, tra cui quella dettasingle sign on, la quale permette ad un fornitore di servizi di mettere a dispo-sizione degli utenti un insieme di applicazioni a cui si puo accedere effettuandol’autenticazione una sola volta. Anche Google ha adottato questa soluzioneper Google Apps, solo che ha implementato una sua versione del protocollodi autenticazione, discostandosi dallo standard. Tale implementazione, pero,e soggetta ad un attacco, descritto per la prima volta in [1], che permette adun intruso di avere accesso a delle risorse confidenziali.

Lo scopo del lavoro svolto e la formalizzazione del protocollo SAML diGoogle in HLPSL, un linguaggio nato per formalizzare protocolli di sicurezza,in modo da poter verificare se Avispa, un tool per l’analisi della correttezza diprotocolli Internet, e in grado di rilevare l’attacco a cui e vulnerabile GoogleApps.

Nel primo capitolo si procede introducendo le principali caratteristiche diSAML, la variante del protocollo implementata da Google e l’attacco a cuiquesta e soggetta. Nel secondo capitolo, invece, si prosegue con la descrizionedella formalizzazione del protocollo in HLPSL effettuata. Il terzo capitoloillustra i risultati ottenuti dall’analisi fatta da Avispa sulla formalizzazionefatta; Avispa dispone di quattro analizzatori, tuttavia e stato possibile testare

1

2 Introduzione

il codice scritto solo con tre di questi. Il quarto capitolo contiene la descrizionedella nuova versione del protocollo SAML adottata da Google dopo la scopertadell’esistenza dell’attacco qui descritto; in questo capitolo si descrive anche laformalizzazione fatta del nuovo protocollo ed i risultati ottenuti con Avispa.Nel capitolo conclusivo si commenteranno i risultati ottenuti, mentre nelle dueappendici, infine, sono riportati il codice sorgente scritto ed gli output prodottida Avispa.

Capitolo 2

SAML SSO

In questo capitolo verra introdotto il funzionamento del protocollo SAML SSO,in particolare nella prima sezione si spieghera il funzionamento della versio-ne standard del protocollo, mentre nella restante parte del capitolo verran-no introdotte le caratteristiche dell’implementazione di Google e del relativoattacco.

2.1 Il protocollo SAML SSO

SAML (acronimo per Security Assertion Markup Language) e un’applicazioneXML che permette lo scambio di messaggi autenticati e confidenziali tra duedomini, in particolare tra un identity provider, colui che produce le asserzioni,ed un service provider, il destinatario di tali asserzioni. Questa applicazione egestita da OASIS, che ne cura lo standard ufficiale e rilascia le nuove versioniufficiali della stessa (per maggiori dettagli vedere [2]).

SAML si basa su due concetti fondamentali, il binding e i profili; per bindingsi intende il modo in cui le asserzioni vengono mappate in messaggi di unprotocollo di trasmissione od in un formato standard di messaggi. La versioneattuale del linguaggio, la 2.0, supporta i bindings per i seguenti protocolli:

• SAML SOAP (basato su SOAP 1.1);

• Reverse SOAP (PAOS);

• HTTP Redirect (GET);

• HTTP POST;

• HTTP Artifact;

• SAML URI.

3

4 SAML SSO

Un profilo, invece, e la descrizione dettagliata di come organizzare gli ele-menti SAML per ottenere una certa funzionalita; la versione 2.0 del linguaggioprevede i seguenti profili:

• profili SSO:

– Web Browser SSO;

– Enhanced Client or Proxy (ECP);

– Identity Provider Discovery;

– Single Logout;

– Name Identifier Management;

• Artifact Resolution;

• Assertion Query/Request;

• Name Identifier Mapping;

• SAML Attribute.

In questo scritto ci si concentrera sul profilo piu usato, il single sign on,SSO in breve, in particolare nella variante web browser.

I protocolli SSO sono nati con lo scopo di permettere ad un utente di auten-ticarsi in un ambiente contenente diversi servizi. In questo modo si semplificala gestione delle credenziali di accesso, sia per gli erogatori di servizi, che do-vranno memorizzare una sola coppia username-password per persona, sia pergli utenti, i quali dovranno autenticarsi una sola volta per fruire poi di piuservizzi liberamente.

Un esempio di applicazione di un protocollo SSO e quello di Google Apps,dove l’utente, una volta autenticatosi, ha accesso a diversi servizi, quali Gmail,Google Calendar, Talk, Docs e Sites, potendo passare da un’applicazioneGoogle all’altra, senza riautenticarsi.

Il profilo SSO di SAML ed il protocollo (in questo contesto per protocol-lo si intende il modo in cui gli elementi SAML devono essere elaborati perraggiungere un certo scopo) authentication request forniscono proprio questafunzionalita. La figura 2.1 mostra come avviene una sessione del protocolloauthentication request di SAML nella variante in cui l’inizializzazione vienefatta dal fornitore di servizi (SP-Initiated SSO con Redirect/POST Bindings).Gli attori del protocollo sono tre, un client (C) che richiede una risorsa adun service provider (SP) ed un identity provider (IDP) che ha il compito diautenticare C per SP.

2.1 Il protocollo SAML SSO 5

Figura 2.1: Una sessione SAML SSO

6 SAML SSO

La sessione inizia con il client che effettua una richiesta di una risorsa al ser-vice provider, questi risponde con una richiesta di autenticazione che il clientinoltra all’identity provider; IDP ha il compito di autenticare C, cio avvieneattraverso l’inserimento di uno username e di una password oppure in un qual-siasi altro modo. Una volta che l’identity provider ha verificato l’identita di Cgenera e firma una risposta, contenente l’asserzione di autenticazione per C,che invia al client; questi inoltra il messaggio ricevuto al service provider, ilquale in questo modo puo essere sicuro dell’identita di C e quindi procede conl’invio delle risorse richieste al client.

Il protocollo assume che sia IDP che SP siano autenticati per C, questoavviene attraverso lo scambio di certificati X.509 e l’uso del protocollo SSLper garantire la sicurezza dei canali, in particolare:

1. le comunicazioni tra C ed SP avvengono attraverso un canale unilateraleSSL 3.0, cioe il service provider deve fornire il suo certificato al client;

2. le comunicazioni tra C ed IDP si effettuano attraverso un canale SSL cheinizialmente e unilaterale, in quanto solo IDP fornisce il suo certificato aC, ma che poi diventa bilaterale quando C fornisce le sue credenziali diautenticazione all’identity provider.

Come ultima cosa va specificato che cio che si vuole ottenere dopo la ses-sione della figura 2.1 e che SP autentichi C e che le risorse rimangano segretetra questi due agenti.

2.2 Implementazione Google di SAML ed il

relativo attacco

L’interpretazione di Google del protocollo SAML SSO, descritta in [1], ap-pare diversa da quella riportata nella figura 2.1 per alcuni particolari che, sepur a prima vista possono sembrare irrilevanti, invece rendendolo il proto-collo vulnerabile ad un attacco. La figura 2.2 mostra la variante Google delprotocollo.

Come si puo evincere dall’immagine vi sono due differenze con la sessioneSAML descritta nella sezione precedente: la prima e che l’authentication as-sertion non comprende piu ne ID ne SP, la seconda e che la risposta generatada IDP non comprende piu i campi ID ed IDP.

Il fatto di non includere piu SP nell’authentication assertion, generata dal-l’identity provider, e il fattore che rende il protocollo vulnerabile ad un attacco,il quale viene effettuato da un intruso che impersona un service provider male-volo. La figura 2.3 mostra lo schema dell’attacco, scoperto molto recentemente

2.2 Implementazione Google di SAML ed il relativo attacco 7

Figura 2.2: Una sessione Google di SAML SSO

8 SAML SSO

da Armando et al. (per maggiori dettagli vedere [1]); le frecce piu grosse sonoi messaggi inviati dall’intruso.

Figura 2.3: Attacco all’implementazione SAML SSO di Google

L’attacco si ottiene combinando insieme due sessioni, la prima in cui l’intru-so gioca il ruolo di service provider e la seconda dove invece funge da client. Leazioni che l’intruso deve intraprendere per eseguire l’attacco sono le seguenti:

1. prima di tutto deve diventare un service provider fidato per un client, inmodo da poter stabilire con lui un canale SSL;

2. appena riceve una richiesta da parte del client lo inoltra a Google cam-biando l’URI di partenza in uno relativo ad un servizio di Google Apps(ad esempio Gmail);

3. quando riceve da SP la richiesta di autenticazione, l’intruso la inoltra alvero client, cambiando l’ID con uno nuovo e inserendo l’URI richiestoda C al posto di quello di Google Apps, in modo tale che questi possaprocedere alla propria autenticazione attraverso l’IDP;

4. ricevuta la risposta dal client, l’attaccante la spedisce a Google avendocura di cambiare I con Google e l’URI originale con quello della risorsache desidera ricevere;

5. a questo punto, come ultima cosa, l’attacante deve aspettare che SP gliinvii le risorse di Google Apps.

2.2 Implementazione Google di SAML ed il relativo attacco 9

Alla fine di questo scambio di messaggi l’attacco e terminato e l’intrusoha avuto accesso a delle risorse che dovevano restare segrete tra C e Google,ingannando quest ultimo sulla sua vera identita.

10 SAML SSO

Capitolo 3

Formalizzazione di SAML inHLPSL

In questo capitolo verra discussa la modellazione della versione SAML SSOimplementata da Google in HLPSL (acronimo di high level protocol securi-ty language), linguaggio adottato da Avispa per analizzare la correttezza deiprotocolli di sicurezza. Per maggiori informazioni su Avispa e sull’uso del lin-guaggio HLPSL, si possono consultare [4] e [5], che forniscono tutte le nozionifondamentali su questi temi.

Il primo problema in cui si incorre volendo formalizzare in HLPSL SAMLe quello della modellazione dei canali SSL, in quanto il linguaggio non forni-sce questa tipologia di canale, ma rende disponibile solo il modello del canaleDolev-Yao, secondo il quale l’intruso ha il pieno controllo di cio che transitaattraverso il canale di trasmissione, puo alterare il contenuto dei messaggi, in-viarne di nuovi e venire a conoscenza di ogni messaggio che attraversa il canaledi trasmissione. Per risolvere questo problema, si e pensato a due soluzioni:la prima prevede la cifratura di tutti i messaggi attraverso delle chiavi sim-metriche, il cui valore e noto soltanto a mittente e destinatario del messaggio,la seconda, invece, fa uso della crittografia a chiave pubblica, attraverso laquale ogni messaggio viene autenticato e reso confidenziale. Il codice delle dueformalizzazioni si trova nelle prime due sezioni dell’appendice A.

3.1 Formalizzazione con chiavi simmetriche

In questa sezione si spiegheranno le caratteristiche principali della modellazio-ne del protocollo SAML attraverso la cifratura a chiave simmetrica. Questasoluzione si basa sull’uso di una chiave diversa per ogni coppia di interlocutori,in particolare vi e una chiave condivisa tra C ed SP ed una tra C e IDP. Va

11

12 Formalizzazione di SAML in HLPSL

detto inoltre che anche l’intruso dovra disporre di una chiave per comunicarecon SP, di una per interagire con C e di un’altra chiave per comunicare conIDP (in realta tale chiave risulta inutile al fine di trovare l’attacco ma dovendol’intruso impersonare un client deve essere definita anche tale chiave).

Figura 3.1: Schema di un protocollo in HLPSL

Come mostrato nella figura 3.1, HLPSL prevede che i protocolli venganospecificati definendo dei ruoli semplici, uno per ogni agente che prende parte alprotocollo, e dei ruoli composti che stabiliscono come avviene una sessione delprotocollo preso in esame. Oltre a cio vanno definiti gli obiettivi di sicurezzafissati per il protocollo e le conoscenze di base possedute dall’intruso. Un ruolosemplice in HLPSL, il cui schema e mostrato nella figura 3.2, e composto da

3.1 Formalizzazione con chiavi simmetriche 13

tre parti: la prima e l’intestazione del ruolo in cui si dichiarano i valori diinput (ad esempio gli agenti del protocollo), la seconda e la dichiarazione dellevariabili e delle costanti e la terza e composta dalle transizioni che devonoessere attraversate durante l’esecuzione di una sessione.

Figura 3.2: Struttura di un ruolo semplice

Si procede ora con la descrizione della modellazione dei tre ruoli di base. Ilruolo del client riceve in input i tre agenti (C, IDP, e SP), le chiavi simmetricheper comunicare con SP e IDP, la chiave pubblica di IDP, quattro canali dicomunicazione (due per inviare e due per ricevere dati sia da SP che da IDP) euna funzione di hash che servira a modellare le risorse. Le transizioni effettuatedal client sono le seguenti:

1. si inizia la sessione inviando ad SP un messaggio contenente il valore diC, di SP e l’URI desiderato;

2. quando si riceve la richiesta di autenticazione da parte di SP la si inoltraad IDP;

3. nel momento in cui si riceve la conferma di autenticazione da parte diIDP la si invia a SP;

4. quando si ricevono le risorse (modellate come una funzione hash dell’URI)da SP si raggiunge lo stato finale.

Come gia detto in precedenza, si ricorda che ogni messaggio va cifrato conla relativa chiave simmetrica. Come ultima cosa, nella penultima transizionedel ruolo, va specificata una asserzione di tipo witness in modo da indicareche quando si e giunti a questo punto della sessione il client dovrebbe essersiautenticato nei confronti di SP attraverso il valore di URI.


Il ruolo del service provider riceve in ingresso i valori degli agenti SP eIDP, una chiave simmetrica che deve essere condivisa con il client, due canalidi trasmissione (da e verso C), la chiave pubblica di IDP e la funzione pergenerare le risorse. Le transizioni sono le seguenti:

1. quando si riceve una richiesta di risorse da parte del client, si rispondecon l’invio di una richiesta di autenticazione;

2. se arriva una conferma di autenticazione firmata da IDP e provenientedal client, si procede con l’invio delle relative risorse precedentementerichieste da C.

All’ultima transizione vanno aggiunte due asserzioni di sicurezza, una ditipo request, per indicare che giunti a questo punto SP deve aver autenticatoC attraverso il valore di URI, e l’altra di tipo secret indicante che le risorsedevono restare segrete tra C ed SP.

Il ruolo dell’identity provider riceve in ingresso i tre agenti del protocollo,una chiave simmetrica per comunicare con il client, la sua chiave pubblica eduna coppia di canali per comunicare con C. IDP ha solo una transizione daeseguire che si attiva quando l’agente riceve una richiesta di autenticazione daparte del client; a tale richiesta, l’identity provider risponde con un messaggiocontenente:

• il nome del service provider che ha fatto richiesta di autenticazione;

• i valori di C ed IDP firmati con la sua chiave privata (KIDP);

• l’URI per il quale era stata richiesta l’autenticazione.

Oltre ai tre ruoli appena descritti ve ne sono altri due composti. Il primoruolo e chiamato session e riceve in ingresso i tre agenti, tutte le chiavi di ci-fratura previste dalla modellazione e la funzione di hash che modella le risorse;all’interno di questo ruolo vengono creati tutti i canali di comunicazione pre-visti e vengono composti i tre ruoli semplici in modo da formare una sessionedel protocollo SAML valida. Il secondo ruolo composto, chiamato enviromentnon ha parametri di ingresso, al suo interno vengono dichiarati, sotto forma dicostanti, i valori relativi ai tre agenti, alle chiavi di cifratura, alla funzione ge-neratrice delle risorse e gli identificatori delle asserzioni di sicurezza. In questoruolo vengono anche dichiarate le informazioni che l’intruso dispone all’iniziodi una sessione, cioe i nomi dei tre agenti (c, sp, idp), le chiavi simmetricheche puo usare (kci, kisp) e la chiave pubblica dell’identity provider (kidp).Il ruolo compone insieme tre sessioni (cioe il ruolo session viene invocato pertre volte) una tra C e l’intruso nel ruolo di service provider, una tra C ed SPe la terza tra l’intruso, che impersona un client, ed SP.

3.2 Formalizzazione con chiavi asimmetriche 15

La modellazione termina con la dichiarazione dei due goals di sicurezzache il protocollo dovrebbe rispettare: il primo indica che le risorse dovrebberorestare segrete tra C ed SP (cio corrisponde all’uso di un’asserzione di tiposecret presente del ruolo del service provider), il secondo che alla fine di unasessione del protocollo C dovrebbe essersi autenticato nei confronti di SP (perquesto goals sono state dichiarate le altre due asserzioni di sicurezza presentinel ruolo del client e in quello del service provider).

3.2 Formalizzazione con chiavi asimmetriche

Questa modellazione risulta molto simile a quella precedentemente illustrata,in particolare la struttura risulta essere la stessa: la formalizzazione contie-ne tre ruoli semplici che modellano il comportamento dei relativi agenti, edue composti usati per simulare una sessione del protocollo; anche i goals disicurezza risultano essere i medesimi. Rispetto alla variante a chiave simme-trica, il cambiamento piu significativo e il modo in cui vengono modellati icanali SSL, in particolare, dove e richiesta la confidenzialita del canale, i dativengono cifrati con la chiave pubblica del destinatario, mentre se e richiestal’autenticazione, i messaggi vengono firmati con la chiave privata del mittente.L’organizzazione dei canali e la seguente:

• canale da C a SP: i dati sono cifrati con la chiave publica di SP e firmaticon quella privata di C, che viene inviata a SP nel primo messaggio;

• canale da SP a C: i dati sono firmati da SP e cifrati con la chiave pubblicadi C precedentemente inviata a SP (questo canale deve essere fortementeautenticato ma debolmente confidenziale);

• canale da C a IDP: i dati sono cifrati con la chiave pubblica di IDP,l’autenticazione debole e data dall’inserimento di username e passwordda parte di C ;

• canale da IDP a C: questo canale e fortemente confidenziale ed autenti-cato, quindi i dati sono firmati e cifrati.

Ogni agente, e quindi anche l’intruso, deve dunque possedere una chiave pub-blica e una privata (in HLPSL la chiave privata viene ottenuta passando larelativa pubblica come argomento alla funzione inv()).

L’addozione della crittografia a chiave pubbblica ha comportato anche altremodifiche hai ruoli semplici, in particolare ora non ricevono piu in input dellechiavi simmetriche, queste sono state sostituite con le relative chiavi pubbli-che degli agenti che condividono lo stesso canale; per modellare il fatto che


inizialmente C non e autenticato da SP, il client concatena la sua chiave pub-blica al primo messaggio che invia al service provider, cio viene fatto perchese SP conoscesse gia la chiave pubblica di C, allora il client sarebbe gia statoautenticato dal service provider (attraverso l’invio di un certificato X.509 adesempio).

I due ruoli composti vengono modificati sostituendo le chiavi simmetrichecon quelle pubbliche e cambiando la conoscenza di base dell’intruso il qualeora dispone di una coppia di chiavi asimmetriche; dalle conoscenze dell’intrusoviene esclusa la chiave pubblica di IDP, questo viene fatto perche altrimentic’e il rischio che gli analizzatori trovino dei falsi attacchi, dovuti al fatto chel’intruso possa fingersi IDP con C (cio in realta non puo succedere con deicanali SSL reali).

Capitolo 4

Risultati ottenuti con Avispa

In questo capitolo veranno presentati i risultati ottenuti analizzando con Avi-spa le due modellazioni del protocollo SAML introdotte nel capitolo prece-dente. Avispa dispone di quattro analizzatori back-end con cui poter testarei protocolli di sicurezza, in questo caso sono stati impiegati tre analizzatori,ofmc, satmc e cl-atse, in quanto il quarto (ta4sp) non era funzionante nell’in-stallazione di Avispa utilizzata. I risultati ottenuti sono riportati nelle primedue sezioni dell’appendice B

4.1 Risultati della versione a chiavi simmetri-

che

Facendo analizzare ad Avispa la formalizzazione di SAML che modella i canalidi comunicazione attraverso le chiavi simmetriche si ottengono risultati diversiin base all’analizzatore impiegato. Gli analizzatori trovano degli attacchi leg-germente diversi da quello mostrato nella figura 2.3; l’attacco precedentementeillustrato prevede l’uso di due sessioni parallele, una in cui l’intruso impersonaun service provider malevolo e l’altra in cui, invece, gioca il ruolo di client conil service provider reale. Come si puo vedere nella figura 4.1, ofmc rileva unattacco al protocollo che fa uso di due sessioni sequenziali, la prima delle qualie una quasi regolare sessione SAML tra il client e l’intruso nel ruolo di serviceprovider, mentre la seconda vede l’attaccante nel ruolo di client ed il serviceprovider di Google nel suo ruolo naturale. Nella seconda sessione l’intruso usal’authAssert ottenuta nel primo scambio di messaggi con il client per ingannareil service provider ed ottenere le risorse al posto del client. L’altra differenzarilevata e che i messaggi scambiati tra il client e l’identity provider vengonointercettati dall’intruso che li inoltra al giusto (passi 3, 4 , 5, 6 della primasessione), mentre nell’attacco illustrato nel primo capitolo l’attaccante non fa-

17

18 Risultati ottenuti con Avispa

ceva uso di tali messaggi; tuttavia si tratta di una differenza di poco conto inquanto non modifica la tipologia di attacco rilevato ed in ogni caso l’intrusonon potrebbe modificare questi messaggi in quanto cifrati con una chiave a luiignota.

Figura 4.1: L’attacco rilevato da ofmc

L’attacco trovato da satmc e simile a quello rilevato da ofmc, tranne perdue particolari; il primo e che l’uri richiesto dall’attaccante e lo stesso deside-rato dal client originale, il secondo e che le sessioni non sono piu sequenziali,ma la seconda inizia prima che l’intruso inoltri la richiesta di autenticazioneall’identity provider.

L’ultimo analizzatore usato, cl-atse, trova una variante dell’attacco similea quelle rilevate dagli altri due analizzatori, specialmente ofmc, ma con alcunipassaggi in piu che risultano superflui al fine dell’attacco, quindi non fornice lasoluzione ottima. Questi passaggi in piu che vengono forniti in output dall’a-

4.2 Risultati della versione a chiavi asimmetriche 19

Figura 4.2: L’attaco trovato da satmc

nalizzatore formano una terza sessione del protocollo, in cui un secondo clientfa una richiesta di risorse ad un nuovo service provider, il quale richiede l’au-tenticazione del client ad un altro identity provider, diverso da quello coinvoltonell’attacco; i messaggi scambiati tra queste tre entita sono filtrati dall’intruso,il quale, tuttavia, non puo modificarli in quanto ignaro delle chiavi di cifra-tura usate dagli agenti. La figura 4.3 mostra lo schema dell’attacco appenadescritto, dove C2, IDP2, SP2 sono gli agenti della terza sessione superflua.

4.2 Risultati della versione a chiavi asimme-

triche

I risultati ottenuti con la modellazione del protocollo SAML mediante chiaviassimmetriche sono un po’ diversi da quelli descritti nella precedente sezione.L’unico risultato comune ad entrambe le formalizzazioni e quello fornito daofmc, infatti, anche nel caso della modellazione qui presa in esame, l’attaccorilevato e quello descritto nella figura 4.1.

Un risultato completamente diverso e stato ottenuto usando come analiz-zatore satmc, il quale giudica erroneamente il protocollo safe. Questo e dovutoal fatto che il limite superiore dello spazio di ricerca viene raggiunto prima di


Figura 4.3: L’attacco trovato da cl-atse nel caso simmetrico

4.2 Risultati della versione a chiavi asimmetriche 21

trovare l’attacco. Cl-atse, invece, rileva una variante dell’attacco non trovatain precedenza, in cui vi sono dei passi superflui e per tanto non risulta esse-re una soluzione ottimale. Il risultato ottenuto, mostrato nella figura 4.4, eformato da quattro sessioni SAML, di cui due appartenenti all’attacco e altredue, inutili ed incomplete, fra un service provider e l’intruso, e tra l’intruso edun client. La soluzione rilevata, presenta anche un ordine dei messaggi scam-biati leggermente diverso da quello dell’attacco descritto nel primo capitolo, inparticolare l’intruso inizia la sessione con il service provider mentre il client eancora in attesa della risposta dell’identity provider. Infine anche in questo ca-so i messaggi tra il client e l’identity provider sono intercettati dall’attaccanteil quale provvede ad inoltrarli a destinazione.

Figura 4.4: L’attacco trovato da cl-atse nel caso asimmetrico

Capitolo 5

L’implementazione corretta diGoogle

Dopo essere stata avvisata da Armando et al dell’attacco riguardante la suaimplementazione del protocollo SAML, Google ha prontamente corretto il pro-blema di sicurezza introducendo una nuova versione del protocollo descritta in[3]. In questa sezione si discutera della nuova soluzione e della sua formaliz-zazione in HLPSL il cui codice si trove nelle ultime due sezioni dell’appendiceA.

5.1 La nuova versione di SAML

Come gia fatto presente nel primo capitolo, la vulnerabilita dell’implementazio-ne Google di SAML sta nel fatto di aver ridotto il contenuto dell’authAssertai soli valori di C ed IDP. Per risolvere il problema, Google ha modificatol’authAssert, includendo anche il valore di SP.

La figura 5.1 illustra come la correzione apportata da Google impediscal’attacco precedentemente illustrato. Se l’identity provider firma anche il no-me del service provider che ha richiesto l’autenticazione del client, il serviceprovider ha modo di accorgersi che l’authAssert non e stata generata per luie non procede con l’invio delle risorse. L’intruso, inoltre, non ha modo di ma-nipolare la risposta generata dall’identity provider in quanto questa e firmatacon una chiave privata che non ha modo di reperire.

Per verificare formalmente la correttezza della modifica apportata, sonostate fatte due modellazioni della stessa in HLPSL. Le due modellazioni diffe-riscono, ancora una volta, soltanto per il modo di modellare i canali SSL, per-tanto le modifiche da apportare alle formalizzazioni gia descritte in precedenzasono minime. Cio che e stato fatto e cambiare le transizioni relative all’invio,

23

24 L’implementazione corretta di Google

Figura 5.1: La nuova versione Google di SAML

od alla ricezione, della risposta dell’IDP, in modo che l’authAssert includes-se anche il valore di SP. Se ad esempio la transizione del ruolo dell’identityprovider nella versione a chiavi simmetriche era

1.State=7 /\ RCV({C.IDP.(ID’.SP).URI’}_KCIDP) =|> State’:=9/\ SND({SP.{(C.IDP)}_inv(KIDP).URI’}_KCIDP) ,

ora nella nuova versione diventa1.State=7 /\ RCV({C.IDP.(ID’.SP).URI’}_KCIDP) =|> State’:=9

/\ SND({SP.{(C.IDP.SP)}_inv(KIDP).URI’}_KCIDP) .

Usando i tre analizzatori di Avispa gia sfruttati in precededenza, si trovasempre lo stesso risultato, per entrambe le formalizzazioni: ora il protocollorisulta safe, anche se pure in questo caso satmc raggiunge il limite di ricercaper entrambe le modellazioni, quindi la sua risposta non e da considerarsiaffidabile. Nelle ultime due sezioni dell’appendice B si riportano tutti i risultatidelle analisi fatte.

Capitolo 6

Conclusione

In questo lavoro si e modellato in HLPSL il protocollo di autenticazione SAMLSSO usato da Google Apps, al fine di verificare se Avispa fosse in grado ditrovare l’attacco esistente per tale implementazione. Come prima cosa, sisono introdotte le principali caratteristiche di SAML, poi ci si e concentratimaggiormente sul profilo SSO, spiegando in che modo si riesca ad autenticareun client, grazie ad un identity provider che svolge il compito di garante trail client stesso ed il service provider a cui e stata fatta la richiesta di risorse;successivamente si e passati a descrivere la variante Google di SAML SSO,illustrando l’attacco a cui quest’ultima e vulnerabile.

Il passo svolto successivamente e stato l’implementazione in HLPSL delprotocollo, dove la difficolta maggiore e stata quella di modellare i canali ditrasmissione SSL, in quanto il linguaggio non fornisce nativamente questa ti-pologia di canali. Per risolvere questo problema sono state create due mo-dellazioni differenti, una facente uso della crittografia a chiave simmetrica perrealizzare i canali sicuri e un’altra che invece, per lo stesso motivo, adotta lacifratura assimmetrica.

Dopo aver realizzato le due formalizzazioni, si e proceduto facendole analiz-zare ad Avispa, facendo uso di tre dei quattro analizzatori di cui il programmapuo far uso: ofmc, satmc e cl-atse. I risultati ottenuti sono simili, tutti glianalizzatori trovano l’attacco od una sua variante, ma ofmc trova la soluzionemigliore, cioe quella con il numero minore di messaggi superflui. Solo satmc,giudica erroneamente corretta la modellazione facente uso della crittografia achiave asimmetrica, a causa del fatto che viene raggiunto il limite superioredello spazio di analisi.

Il lavoro si e concluso con l’illustrazione della nuova versione di SAMLSSO realizzata da Google per risolvere il problema di sicurezza; la correzioneapportata e quella di modificare l’authAssert generata dall’identity providerfacendo in modo di includere in questa anche l’identita del service provider

25

26 Conclusione

che richiede l’autenticazione del client. In questo modo il protocollo risultacorretto, infatti formalizzandolo in HLPSL (sempre usando due varianti per lamodellazione dei canali) e facendolo analizzare da Avispa non si trovano piuattacchi, anche se la risposta di satmc non risulta attendibile.

Si desidera, infine, ringraziare i prof. Armando e Carbone per i loro sugge-rimenti su una versione preliminare dell’implementazione.

Appendice A

Codice sorgente prodotto

In questa appendice viene riportato il codice HLPSL prodotto per formalizzareSAML SSO. Il codice e relativo a quattro sorgenti, divisi in base al tipo di mo-dellazione dei canali SSL e in base alla variante del protocollo che modellano,cioe quella corretta o quella sbagliata.

A.1 Sorgente della versione errata a chiavi sim-

metriche

role client(C,IDP,SP:agent,KCSP,KCIDP:symmetric_key,KIDP:public_key,SSP,RSP,SIDP,RIDP:channel(dy),Resource:hash_func)

played_by C def=local

State: nat,AA:(agent.agent),URI,ID:text

init State:=0transition

1.State=0 /\ RSP(start) =|> State’:=2 /\ URI’:=new()/\ SSP({C.SP.URI’}_KCSP)

2.State=2 /\ RSP({C.IDP.(ID’.SP).URI}_KCSP) =|>State’:=4 /\ SIDP({C.IDP.(ID’.SP).URI}_KCIDP)

3.State=4 /\ RIDP({SP.{AA’}_inv(KIDP).URI}_KCIDP) =|>State’:=6 /\ SSP({SP.{AA’}_inv(KIDP).URI}_KCSP)/\ witness(C,SP,c_sp_aa,URI)

27

28 Codice sorgente prodotto

4.State=6 /\ RSP({Resource(URI)}_KCSP) =|> State’:=8end role

role serviceProvider(IDP,SP:agent,KCSP:symmetric_key,KIDP:public_key,SND, RCV:channel(dy),Resource:hash_func)

played_by SP def=local

State:nat,C:agent,ID:text,URI:text

init State:=1transition1.State=1 /\ RCV({C’.SP.URI’}_KCSP) =|> State’:=3

/\ ID’:=new() /\ SND({C’.IDP.(ID’.SP).URI’}_KCSP)2.State=3 /\ RCV({SP.{(C.IDP)}_inv(KIDP).URI}_KCSP) =|>

State’:=5 /\ SND({Resource(URI)}_KCSP)/\ request(SP,C,c_sp_aa,URI)/\ secret(Resource(URI),c_sp_resource,{C,SP})

end role

role identityProvider(C,IDP,SP:agent,KCIDP:symmetric_key,KIDP:public_key,SND,RCV:channel(dy))

played_by IDP def=local

ID,URI:text,State:nat

init State:=7transition1.State=7 /\ RCV({C.IDP.(ID’.SP).URI’}_KCIDP) =|> State’:=9 /\SND({SP.{(C.IDP)}_inv(KIDP).URI’}_KCIDP)

end role

role session(C,IDP,SP:agent,KCSP,KCIDP: symmetric_key,

A.2 Sorgente della versione errata a chiavi asimmetriche 29

KIDP:public_key,Resource:hash_func)

def=local SCSP,RCSP,SCIDP,RCIDP: channel(dy)composition

client(C,IDP,SP,KCSP,KCIDP,KIDP,SCSP,RCSP,SCIDP,RCIDP,Resource) /\serviceProvider(IDP,SP,KCSP,KIDP,SCSP,RCSP,Resource) /\

identityProvider(C,IDP,SP,KCIDP,KIDP,SCIDP,RCIDP)end role

role enviroment()def=

const c_sp_resource,c_sp_aa,id:protocol_id,c,idp,sp:agent,kcsp,kcidp,kci,kisp,kiidp:symmetric_key,kidp:public_key,resource:hash_func

intruder_knowledge={c,idp,sp,kci,kisp,kidp}composition

session(c,idp,i,kci,kcidp,kidp,resource)/\session(c,idp,sp,kcsp,kcidp,kidp,resource)/\session(i,idp,sp,kisp,kiidp,kidp,resource)

end role

goalsecrecy_of c_sp_resourceauthentication_on c_sp_aa

end goal

enviroment()

A.2 Sorgente della versione errata a chiavi asim-

metriche

role client(C,IDP,SP:agent,KC,KSP,KIDP:public_key,SSP,RSP,SIDP,RIDP:channel(dy),Resource:hash_func)



State: nat,ID,URI:text

const c_sp_aa: protocol_idinit State:=0transition1.State=0 /\ RSP(start) =|> State’:=2 /\URI’:=new()

/\ SSP({KC.C.SP.URI’}_KSP)2.State=2 /\ RSP({{C.IDP.(ID’.SP).URI}_inv(KSP)}_KC) =|>

State’:=4 /\ SIDP({C.IDP.(ID’.SP).URI}_KIDP)3.State=4 /\ RIDP({{SP.{(C.IDP)}_inv(KIDP).URI}_inv(KIDP)}_KC) =|>

State’:=6 /\ SSP({{SP.{(C.IDP)}_inv(KIDP).URI}_inv(KC)}_KSP)/\ witness(C,SP,c_sp_aa,URI)

4.State=6 /\ RSP({{Resource(URI)}_inv(KSP)}_KC) =|>State’:=8end role

role serviceProvider(C,IDP,SP:agent,KSP,KIDP:public_key,SND, RCV:channel(dy),Resource:hash_func)


State:nat,ID:text,KC:public_key,URI:text

init State:=1transition1.State=1 /\ RCV({KC’.C.SP.URI’}_KSP) =|> State’:=3 /\ ID’:=new()

/\ SND({{C.IDP.(ID’.SP).URI’}_inv(KSP)}_KC’)2.State=3 /\ RCV({{SP.{(C.IDP)}_inv(KIDP).URI}_inv(KC)}_KSP) =|>

State’:=5 /\ SND({{Resource(URI)}_inv(KSP)}_KC)/\ request(SP,C,c_sp_aa,URI)/\ secret(Resource(URI),c_sp_resource,{C,SP})

end role

role identityProvider(C,IDP,SP:agent,KC,KIDP:public_key,SND,RCV:channel(dy))

played_by IDP def=

A.2 Sorgente della versione errata a chiavi asimmetriche 31

localID:text,URI:text,State:nat

init State:=7transition1.State=7 /\ RCV({C.IDP.(ID’.SP).URI’}_KIDP) =|> State’:=9

/\ SND({{SP.{(C.IDP)}_inv(KIDP).URI’}_inv(KIDP)}_KC)end role

%regole composte

role session(C,IDP,SP:agent,KC,KSP,KIDP:public_key,Resource:hash_func)


client(C,IDP,SP,KC,KSP,KIDP,SCSP,RCSP,SCIDP,RCIDP,Resource) /\serviceProvider(C,IDP,SP,KSP,KIDP,SCSP,RCSP,Resource) /\identityProvider(C,IDP,SP,KC,KIDP,SCIDP,RCIDP)

end role


const c_sp_resource,c_sp_aa,id:protocol_id,c,idp,sp:agent,kc,ksp,kidp,ki:public_key,resource:hash_func

intruder_knowledge={c,sp,ksp,ki,inv(ki),idp,resource}composition

session(c,idp,i,kc,ki,kidp,resource)/\session(c,idp,sp,kc,ksp,kidp,resource)/\session(i,idp,sp,ki,ksp,kidp,resource)

end role


end goal

enviroment()


A.3 Sorgente della versione corretta a chiavi

simmetriche

role client(C,IDP,SP:agent,KCSP,KCIDP:symmetric_key,KIDP:public_key,SSP,RSP,SIDP,RIDP:channel(dy),Resource:hash_func)


State: nat,AA:(agent.agent.agent),URI,ID:text

init State:=0transition1.State=0 /\ RSP(start) =|> State’:=2 /\ URI’:=new()

/\ SSP({C.SP.URI’}_KCSP)2.State=2 /\ RSP({C.IDP.(ID’.SP).URI}_KCSP) =|>

State’:=4 /\ SIDP({C.IDP.(ID’.SP).URI}_KCIDP)3.State=4 /\ RIDP({SP.{AA’}_inv(KIDP).URI}_KCIDP) =|>

State’:=6 /\ SSP({SP.{AA’}_inv(KIDP).URI}_KCSP)/\ witness(C,SP,c_sp_aa,URI)

4.State=6 /\ RSP({Resource(URI)}_KCSP) =|>State’:=8end role

role serviceProvider(IDP,SP:agent,KCSP:symmetric_key,KIDP:public_key,SND, RCV:channel(dy),Resource:hash_func)


State:nat,C:agent,ID:text,URI:text


A.3 Sorgente della versione corretta a chiavi simmetriche 33

1.State=1 /\ RCV({C’.SP.URI’}_KCSP) =|> State’:=3 /\ ID’:=new()/\ SND({C’.IDP.(ID’.SP).URI’}_KCSP)

2.State=3 /\ RCV({SP.{(C.IDP.SP)}_inv(KIDP).URI}_KCSP) =|>State’:=5/\ SND({Resource(URI)}_KCSP)/\ request(SP,C,c_sp_aa,URI) /\secret(Resource(URI),c_sp_resource,{C,SP})

end role

role identityProvider(C,IDP,SP:agent,KCIDP:symmetric_key,KIDP:public_key,SND,RCV:channel(dy))


ID,URI:text,State:nat


1.State=7 /\ RCV({C.IDP.(ID’.SP).URI’}_KCIDP) =|> State’:=9/\ SND({SP.{(C.IDP.SP)}_inv(KIDP).URI’}_KCIDP)

end role

role session(C,IDP,SP:agent,KCSP,KCIDP: symmetric_key,KIDP:public_key,Resource:hash_func)


client(C,IDP,SP,KCSP,KCIDP,KIDP,SCSP,RCSP,SCIDP,RCIDP,Resource) /\serviceProvider(IDP,SP,KCSP,KIDP,SCSP,RCSP,Resource) /\identityProvider(C,IDP,SP,KCIDP,KIDP,SCIDP,RCIDP)

end role


const c_sp_resource,c_sp_aa,id:protocol_id,c,idp,sp:agent,kcsp,kcidp,kci,kisp,kiidp:symmetric_key,kidp:public_key,resource:hash_func


intruder_knowledge={c,idp,sp,kci,kisp,kidp}compositionsession(c,idp,i,kci,kcidp,kidp,resource)

/\session(c,idp,sp,kcsp,kcidp,kidp,resource)/\session(i,idp,sp,kisp,kiidp,kidp,resource)

end role


end goal

enviroment()

A.4 Sorgente della versione corretta a chiavi

asimmetriche

role client(C,IDP,SP:agent,KC,KSP,KIDP:public_key,SSP,RSP,SIDP,RIDP:channel(dy),Resource:hash_func)

played_by C def=localState: nat,ID,URI:text

const c_sp_aa: protocol_idinit State:=0transition1.State=0 /\ RSP(start) =|> State’:=2 /\URI’:=new()

/\ SSP({KC.C.SP.URI’}_KSP)2.State=2 /\ RSP({{C.IDP.(ID’.SP).URI}_inv(KSP)}_KC) =|>

State’:=4 /\ SIDP({C.IDP.(ID’.SP).URI}_KIDP)3.State=4 /\ RIDP({{SP.{(C.IDP.SP)}_inv(KIDP).URI}_inv(KIDP)}_KC) =|>

State’:=6 /\ SSP({{SP.{(C.IDP.SP)}_inv(KIDP).URI}_inv(KC)}_KSP)/\ witness(C,SP,c_sp_aa,URI)

4.State=6 /\ RSP({{Resource(URI)}_inv(KSP)}_KC) =|>State’:=8end role

role serviceProvider(C,IDP,SP:agent,

A.4 Sorgente della versione corretta a chiavi asimmetriche 35

KSP,KIDP:public_key,SND, RCV:channel(dy),Resource:hash_func)

played_by SP def=localState:nat,ID:text,KC:public_key,URI:text

init State:=1transition1.State=1 /\ RCV({KC’.C.SP.URI’}_KSP) =|> State’:=3 /\ ID’:=new()

/\ SND({{C.IDP.(ID’.SP).URI’}_inv(KSP)}_KC’)2.State=3 /\ RCV({{SP.{(C.IDP.SP)}_inv(KIDP).URI}_inv(KC)}_KSP) =|>

State’:=5 /\ SND({{Resource(URI)}_inv(KSP)}_KC) /\request(SP,C,c_sp_aa,URI) /\secret(Resource(URI),c_sp_resource,{C,SP})

end role

role identityProvider(C,IDP,SP:agent,KC,KIDP:public_key,SND,RCV:channel(dy))


ID:text,URI:text,State:nat

init State:=7transition1.State=7 /\ RCV({C.IDP.(ID’.SP).URI’}_KIDP) =|> State’:=9/\ SND({{SP.{(C.IDP.SP)}_inv(KIDP).URI’}_inv(KIDP)}_KC)

end role

%regole composte

role session(C,IDP,SP:agent,KC,KSP,KIDP:public_key,Resource:hash_func)



client(C,IDP,SP,KC,KSP,KIDP,SCSP,RCSP,SCIDP,RCIDP,Resource) /\serviceProvider(C,IDP,SP,KSP,KIDP,SCSP,RCSP,Resource) /\identityProvider(C,IDP,SP,KC,KIDP,SCIDP,RCIDP)

end role


const c_sp_resource,c_sp_aa,id:protocol_id,c,idp,sp:agent,kc,ksp,kidp,ki:public_key,resource:hash_func

intruder_knowledge={c,sp,ksp,ki,inv(ki),idp,resource}compositionsession(c,idp,i,kc,ki,kidp,resource)/\session(c,idp,sp,kc,ksp,kidp,resource)/\session(i,idp,sp,ki,ksp,kidp,resource)

end role


end goal

enviroment()

Appendice B

Output di Avispa

In questa appendice sono riportati gli output forniti da Avispa analizzando le quattroformalizzazioni di SAML realizzate. Le risposte di Avispa sono divise in base allaformalizzazione e all’analizzatore usato per ottenerle.

B.1 Output della versione errata a chiavi sim-

metriche

B.1.1 Output di ofmc

[guest@localhost labRcs]$ avispa samlUnsafe.hlpsl --ofmc% OFMC% Version of 2006/02/13SUMMARYUNSAFE

DETAILSATTACK_FOUND

PROTOCOL/union/home/guest/avispa-1.1/testsuite/results/samlUnsafe.if

GOALsecrecy_of_c_sp_resource

BACKENDOFMC

COMMENTSSTATISTICSparseTime: 0.00ssearchTime: 0.10svisitedNodes: 37 nodesdepth: 5 plies

ATTACK TRACE

37

38 Output di Avispa

i -> (c,3): start(c,3) -> i: {c.i.URI(1)}_kcii -> (c,3): {c.idp.x253.i.URI(1)}_kci(c,3) -> i: {c.idp.x253.i.URI(1)}_kcidpi -> (idp,5): {c.idp.x253.i.URI(1)}_kcidp(idp,5) -> i: {i.{c.idp}_inv(kidp).URI(1)}_kcidpi -> (c,3): {i.{c.idp}_inv(kidp).URI(1)}_kcidp(c,3) -> i: {i.{c.idp}_inv(kidp).URI(1)}_kcii -> (sp,12): {c.sp.x278}_kisp(sp,12) -> i: {c.idp.ID(5).sp.x278}_kispi -> (sp,12): {sp.{c.idp}_inv(kidp).x278}_kisp(sp,12) -> i: {resource(x278)}_kispi -> (i,17): resource(x278)i -> (i,17): resource(x278)

% Reached State:%% secret(resource(x278),c_sp_resource,set_109)% contains(c,set_109)% contains(sp,set_109)% witness(c,i,c_sp_aa,URI(1))% state_identityProvider(idp,i,sp,kiidp,kidp,dummy_nonce,dummy_nonce,7,12)% state_serviceProvider(sp,idp,kisp,kidp,resource,5,c,ID(5),x278,set_109,12)% state_identityProvider(idp,c,sp,kcidp,kidp,dummy_nonce,dummy_nonce,7,7)% state_serviceProvider(sp,idp,kcsp,kidp,resource,1,dummy_agent,dummy_nonce,dummy_nonce,set_103,7)% state_client(c,idp,sp,kcsp,kcidp,kidp,resource,0,dummy_agent.dummy_agent,dummy_nonce,dummy_nonce,7)% state_identityProvider(idp,c,i,kcidp,kidp,x253,URI(1),9,5)% state_client(c,idp,i,kci,kcidp,kidp,resource,6,c.idp,URI(1),x253,3)% request(sp,c,c_sp_aa,x278,12)

B.1.2 Output di satmc

[guest@localhost labRcs]$ avispa samlUnsafe.hlpsl --satmcSUMMARY

UNSAFE

DETAILSATTACK_FOUNDBOUNDED_NUMBER_OF_SESSIONSBOUNDED_SEARCH_DEPTH

B.1 Output della versione errata a chiavi simmetriche 39

BOUNDED_MESSAGE_DEPTH

PROTOCOLsamlUnsafe.if

GOALauthentication_on_c_sp_aa(sp,c,uri(c,3),12)

BACKENDSATMC

COMMENTS

STATISTICSattackFound true booleanupperBoundReached false booleangraphLeveledOff no booleansatSolver zchaff solvermaxStepsNumber 30 stepsstepsNumber 7 stepsatomsNumber 587 atomsclausesNumber 2018 clausesencodingTime 0.329 secondssolvingTime 0.0 secondsif2sateCompilationTime 0.22 seconds

ATTACK TRACEi -> (c,3) : start(c,3) -> i : {c.i.uri(c,3)}_kcii -> (c,3) : {c.idp.uri(c,3).i.uri(c,3)}_kci(c,3) -> i : {c.idp.uri(c,3).i.uri(c,3)}_kcidpi -> (sp,12) : {c.sp.uri(c,3)}_kisp(sp,12) -> i : {c.idp.id0(sp,12).sp.uri(c,3)}_kispi -> (idp,5) : {c.idp.uri(c,3).i.uri(c,3)}_kcidp(idp,5) -> i : {i.{c.idp}_inv(kidp).uri(c,3)}_kcidpi -> (c,3) : {i.{c.idp}_inv(kidp).uri(c,3)}_kcidp(c,3) -> i : {i.{c.idp}_inv(kidp).uri(c,3)}_kcii -> (sp,12) : {sp.{c.idp}_inv(kidp).uri(c,3)}_kisp(sp,12) -> i : {resource(uri(c,3))}_kisp

B.1.3 Output di cl-atse

[guest@localhost labRcs]$ avispa samlUnsafe.hlpsl --cl-atse

40 Output di Avispa

SUMMARYUNSAFE

DETAILSATTACK_FOUNDTYPED_MODEL

PROTOCOL/union/home/guest/avispa-1.1/testsuite/results/samlUnsafe.if

GOALSecrecy attack on ({URI(25)}_resource)

BACKENDCL-AtSe

STATISTICS

Analysed : 32 statesReachable : 13 statesTranslation: 0.02 secondsComputation: 0.00 seconds

ATTACK TRACEi -> (c,7): start(c,7) -> i: {c.sp.n11(URI)}_kcsp

i -> (c,3): start(c,3) -> i: {c.i.n1(URI)}_kci

i -> (sp,8): {c.sp.n11(URI)}_kcsp(sp,8) -> i: {c.idp.n19(ID).sp.n11(URI)}_kcsp

i -> (c,7): {c.idp.n19(ID).sp.n11(URI)}_kcsp(c,7) -> i: {c.idp.n19(ID).sp.n11(URI)}_kcidp

i -> (idp,9): {c.idp.n19(ID).sp.n11(URI)}_kcidp(idp,9) -> i: {sp.{c.idp}_(inv(kidp)).n11(URI)}_kcidp

i -> (c,3): {c.idp.ID(2).i.n1(URI)}_kci(c,3) -> i: {c.idp.ID(2).i.n1(URI)}_kcidp

B.2 Output della versione errata a chiavi asimmetriche 41

i -> (idp,5): {c.idp.ID(2).i.n1(URI)}_kcidp(idp,5) -> i: {i.{c.idp}_(inv(kidp)).n1(URI)}_kcidp

i -> (c,3): {i.{c.idp}_(inv(kidp)).n1(URI)}_kcidp(c,3) -> i: {i.{c.idp}_(inv(kidp)).n1(URI)}_kci

i -> (sp,12): {c.sp.URI(25)}_kisp(sp,12) -> i: {c.idp.n25(ID).sp.URI(25)}_kisp

i -> (sp,12): {sp.{c.idp}_(inv(kidp)).URI(25)}_kisp(sp,12) -> i: {{URI(25)}_resource}_kisp

& Secret({URI(25)}_resource,set_109);& Request(sp,c,c_sp_aa,URI(25)); Add c to set_109;& Add sp to set_109;

B.2 Output della versione errata a chiavi asim-

metriche


[guest@localhost labRcs]$ avispa samlUnsafeA.hlpsl --ofmc% OFMC% Version of 2006/02/13SUMMARYUNSAFE

DETAILSATTACK_FOUND

PROTOCOL/union/home/guest/avispa-1.1/testsuite/results/samlUnsafeA.if

GOALsecrecy_of_c_sp_resource

BACKENDOFMC


ATTACK TRACEi -> (c,3): start

42 Output di Avispa

(c,3) -> i: {kc.c.i.URI(1)}_kii -> (c,3): {{idp.x251.i.URI(1)}_inv(ki)}_kc(c,3) -> i: {idp.x251.i.URI(1)}_kidpi -> (idp,5): {idp.x251.i.URI(1)}_kidp(idp,5) -> i: {{i.{c.idp}_inv(kidp).URI(1)}_inv(kidp)}_kci -> (c,3): {{i.{c.idp}_inv(kidp).URI(1)}_inv(kidp)}_kc(c,3) -> i: {{i.{c.idp}_inv(kidp).URI(1)}_inv(kc)}_kii -> (sp,7): {ki.c.sp.x275}_ksp(sp,7) -> i: {{idp.ID(5).sp.x275}_inv(ksp)}_kii -> (sp,7): {{sp.{c.idp}_inv(kidp).x275}_inv(ki)}_ksp(sp,7) -> i: {{resource(x275)}_inv(ksp)}_kii -> (i,17): resource(x275)i -> (i,17): resource(x275)

% Reached State:%% secret(resource(x275),c_sp_resource,set_100)% contains(c,set_100)% contains(sp,set_100)% witness(c,i,c_sp_aa,URI(1))% state_identityProvider(idp,i,sp,ki,kidp,dummy_nonce,dummy_nonce,7,12)% state_serviceProvider(sp,i,idp,ksp,kidp,resource,1,dummy_nonce,dummy_pk,dummy_nonce,set_106,12)% state_identityProvider(idp,c,sp,kc,kidp,dummy_nonce,dummy_nonce,7,7)% state_serviceProvider(sp,c,idp,ksp,kidp,resource,5,ID(5),ki,x275,set_100,7)% state_client(c,idp,sp,kc,ksp,kidp,resource,0,dummy_nonce,dummy_nonce,7)% state_identityProvider(idp,c,i,kc,kidp,x251,URI(1),9,5)% state_client(c,idp,i,kc,ki,kidp,resource,6,x251,URI(1),3)% request(sp,c,c_sp_aa,x275,7)


[guest@localhost labRcs]$ avispa samlUnsafeA.hlpsl --satmcSUMMARY

SAFE

DETAILSBOUNDED_NUMBER_OF_SESSIONSBOUNDED_SEARCH_DEPTHBOUNDED_MESSAGE_DEPTH

PROTOCOL

B.2 Output della versione errata a chiavi asimmetriche 43

samlUnsafeA.if

GOAL%% see the HLPSL specification..

BACKENDSATMC

COMMENTS

STATISTICSattackFound false booleanupperBoundReached true booleangraphLeveledOff 8 stepssatSolver zchaff solvermaxStepsNumber 30 stepsstepsNumber 9 stepsatomsNumber 1043 atomsclausesNumber 3898 clausesencodingTime 0.59 secondssolvingTime 0.0 secondsif2sateCompilationTime 0.29 seconds

ATTACK TRACE%% no attacks have been found..


[guest@localhost labRcs]$ avispa samlUnsafeA.hlpsl --cl-atse

SUMMARYUNSAFE

DETAILSATTACK_FOUNDTYPED_MODEL

PROTOCOL/union/home/guest/avispa-1.1/testsuite/results/samlUnsafeA.if

GOALSecrecy attack on ({URI(19)}_resource)

44 Output di Avispa

BACKENDCL-AtSe

STATISTICS


ATTACK TRACEi -> (c,7): start(c,7) -> i: {kc.c.sp.n11(URI)}_ksp

i -> (c,3): start(c,3) -> i: {kc.c.i.n1(URI)}_ki

i -> (sp,12): {KC(25).i.sp.URI(25)}_ksp(sp,12) -> i: {{idp.n25(ID).sp.URI(25)}_(inv(ksp))}_KC(25)

i -> (c,3): {{idp.ID(2).i.n1(URI)}_(inv(ki))}_kc(c,3) -> i: {idp.ID(2).i.n1(URI)}_kidp

i -> (idp,5): {idp.ID(2).i.n1(URI)}_kidp(idp,5) -> i: {{i.{c.idp}_(inv(kidp)).n1(URI)}_(inv(kidp))}_kc

i -> (sp,8): {ki.c.sp.URI(19)}_ksp(sp,8) -> i: {{idp.n19(ID).sp.URI(19)}_(inv(ksp))}_ki

i -> (c,3): {{i.{c.idp}_(inv(kidp)).n1(URI)}_(inv(kidp))}_kc(c,3) -> i: {{i.{c.idp}_(inv(kidp)).n1(URI)}_(inv(kc))}_ki

i -> (sp,8): {{sp.{c.idp}_(inv(kidp)).URI(19)}_(inv(ki))}_ksp(sp,8) -> i: {{{URI(19)}_resource}_(inv(ksp))}_ki

& Secret({URI(19)}_resource,set_100);& Request(sp,c,c_sp_aa,URI(19)); Add c to set_100;& Add sp to set_100;

B.3 Output della versione corretta a chiavi simmetriche 45

B.3 Output della versione corretta a chiavi sim-

metriche


[guest@localhost labRcs]$ avispa samlSafe.hlpsl --ofmc% OFMC% Version of 2006/02/13SUMMARYSAFE

DETAILSBOUNDED_NUMBER_OF_SESSIONS

PROTOCOL/union/home/guest/avispa-1.1/testsuite/results/samlSafe.if

GOALas_specified

BACKENDOFMC



[guest@localhost labRcs]$ avispa samlSafe.hlpsl --satmcSUMMARYSAFE


PROTOCOLsamlSafe.if


BACKEND

46 Output di Avispa

SATMC

COMMENTS




[guest@localhost labRcs]$ avispa samlSafe.hlpsl --cl-atse

SUMMARYSAFE

DETAILSBOUNDED_NUMBER_OF_SESSIONSTYPED_MODEL

PROTOCOL/union/home/guest/avispa-1.1/testsuite/results/samlSafe.if

GOALAs Specified

BACKENDCL-AtSe

STATISTICS

Analysed : 95 states

B.4 Output della versione corretta a chiavi asimmetriche 47

Reachable : 40 statesTranslation: 0.02 secondsComputation: 0.00 seconds

B.4 Output della versione corretta a chiavi asim-

metriche


[guest@localhost labRcs]$ avispa samlSafeA.hlpsl --ofmc% OFMC% Version of 2006/02/13SUMMARYSAFE

DETAILSBOUNDED_NUMBER_OF_SESSIONS

PROTOCOL/union/home/guest/avispa-1.1/testsuite/results/samlSafeA.if

GOALas_specified

BACKENDOFMC



[guest@localhost labRcs]$ avispa samlSafeA.hlpsl --satmcSUMMARYSAFE


PROTOCOLsamlSafeA.if

48 Output di Avispa


BACKENDSATMC

COMMENTS




[guest@localhost labRcs]$ avispa samlSafeA.hlpsl --cl-atse

SUMMARYSAFE

DETAILSBOUNDED_NUMBER_OF_SESSIONSTYPED_MODEL

PROTOCOL/union/home/guest/avispa-1.1/testsuite/results/samlSafeA.if

GOALAs Specified

BACKEND

B.4 Output della versione corretta a chiavi asimmetriche 49

CL-AtSe

STATISTICS


50 Output di Avispa

Bibliografia

[1] A. Armando, R. Carbone, L. Campagna, J. Cuellar, L. Tobarra Formal Analysisof SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based SingleSign-On for Google Apps. ACM Press (2008).

[2] OASIS Profiles for the OASIS Security Marckup Language (SAML) V2.0.http://docs.oasis-open.org/security/saml/v2.0/ (2005), 14–40.

[3] Google. Web-based reference implementation of SAML-based SSOfor Google Apps. http://code.google.com/apis/sso/saml re-ference implementation web.html (2008).

[4] The Avispa Team A Beginner’s Guide to Modelling and Analysing InternetSecurity Protocols. http://avispa-project.org/ (2006).

[5] The Avispa Team AVISPA v1.1 User Manual. http://avispa-project.org/(2006).

51

FORMALIZZAZIONE DEL PROTOCOLLO SAML SSO …marino.miculan/data/labs/SAMLinHLPSL.… · SAML si basa...

Documents

Transcript of FORMALIZZAZIONE DEL PROTOCOLLO SAML SSO …marino.miculan/data/labs/SAMLinHLPSL.… · SAML si basa...