PROTOCOL:
SAML SSO

VARIANT:
Google unsafe variant; SSL channels modeled using symmetric keys

PURPOSE:
Client authentication in a confidential enviroment
 

REFERENCE:

http:www.ai-lab.it/armando/GoogleSSOVulnerability.html  

MODELER:

 

ALICE_BOB: 

 C->SP:({C.SP.URI}_kcsp)				| Request of a resource
 SP->C:({C.IDP.AuthReq(ID.SP).URI}_kcsp)
 C->IDP:({C.IDP.AuthReq(ID.SP).URI}_kcidp)		| Authentication through an identity provider
 IDP->C:({{C.IDP}_kidp-1.URI}_kcidp)
 C->SP:({{C.IDP}_kidp-1.URI}_kcsp)			| Identity confirmation
 SP->C:({Resource}_kcsp)

 

LIMITATIONS:
The SSL channels are modeled using symmetric keys.

 

PROBLEMS:
2

 

CLASSIFICATION:
G2 G12

 

ATTACKS: 

 C->I:{C.I.URI}_kci
 I->SP:{C.SP.IURI}_kisp
 SP->I:{AuthReq(IDsp.SP).IURI}_kisp
 I->C:{AuthReq(IDi.I).URI}_kci
 C->IDP:{AuthReq(IDi.I).URI}_kcidp
 IDP->C:{{C.IDP}_inv(KIDP).URI}_kcidp
 C->I:{{C.IDP}_inv(KIDP).URI}_kci
 I->SP:{{C.IDP}_inv(KIDP).IURI}_kisp
 SP->I:{Resource(IURI)}_kisp

Double session attack, the first between a client and the intruder as service provider, the second between the intruder as client and a service provider. Intruder can impersonate a honest client and service provider can't realize this

 


HLPSL: 


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:=0
        
        transition
                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)
                4.State=6
                /\ RSP({Resource(URI)}_KCSP) =|>
                State':=8       
end 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:=1
        
        transition
                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)}_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:=7
        
        transition
                1.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,
                                  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}%senza kiidp altrimenti satmc non trova l'attacco
        
        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




goal

 % Confidentiality (G12)
 secrecy_of c_sp_resource

 % Message authentication (G2)
 authentication_on c_sp_aa

end goal




enviroment()