PROTOCOL:
SAML SSO

VARIANT:
Google unsafe variant; SSL channels modeled using asymmetric 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 asymmetric keys. Thus, in principle, this model could yield spurious attacks.

 

PROBLEMS:
2

 

CLASSIFICATION:
G2 G12

 

ATTACKS: 

 C->I:{KC.C.I.URI}_KI
 I->SP:{KI.C.SP.IURI}_KSP
 SP->I:{{IDP.AuthReq(IDsp.SP).IURI}_inv(KSP)}_KI
 I->C:{{IDP.AuthReq(IDi.I).URI}_inv(I)}_KC
 C->IDP:{IDP.(AuthReq(IDi.I).URI}_KIDP
 IDP->C:{{I.{C.IDP}_inv(KIDP).URI}_inv(KIDP)}_KC
 C->I:{{I.{C.IDP}_inv(KIDP).URI}_inv(C)}_KI
 I->SP:{{SP.{C.IDP}_inv(KIDP).IURI}_inv(KI)}_KSP
 SP->I:{{Resource(IURI)}_inv(KSP)}_KI

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,
                  KC,KSP,KIDP:  public_key,
        SSP,RSP,SIDP,RIDP:      channel(dy),
                         Resource:      hash_func) 
played_by C
def=
        local   State:  nat,
                   ID,URI:      text
                   
        const c_sp_aa:  protocol_id
        
        init State:=0
        
        transition
                1.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':=8
end role




role serviceProvider (C,IDP,SP: agent,
                                          KSP,KIDP:     public_key,
                                          SND, RCV:     channel(dy),
                                          Resource:     hash_func)
played_by SP
def=
        local    State: nat,
                                ID:     text,
                                KC:     public_key,
                           URI: text
                           
        init State:=1
        
        transition
                1.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=
        local   ID:     text,
                   URI: text,
                 State: nat
                 
        init State:=7
        
        transition
                1.State=7
                /\ RCV({C.IDP.(ID'.SP).URI'}_KIDP) =|>
                State':=9
                /\ SND({{SP.{(C.IDP)}_inv(KIDP).URI'}_inv(KIDP)}_KC)
end role




role session ( C,IDP,SP:        agent,
                        KC,KSP,KIDP:    public_key,
                           Resource:    hash_func)
def=
        local SCSP,RCSP,SCIDP,RCIDP: channel(dy)
        composition
                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





role enviroment()
def=
        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




goal

 % Confidentiality (G12)
 secrecy_of c_sp_resource

 % Message authentication (G2)
 authentication_on c_sp_aa

end goal




enviroment()