PROTOCOL:
SAML SSO

VARIANT:
Google safe 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:{KC.C.SP.URI}_KSP					| Request of a resource
 SP->C:{{C.IDP.AuthReq(ID.SP).URI}_inv(KSP)}_KIDP
 C->IDP:{C.IDP.AuthReq(ID.SP).URI}_KIDP			| Authentication through an identity provider
 IDP->C:{{SP.{C.IDP.SP}_kidp-1.URI)}_inv(KIDP)}_KC
 C->SP:{{{C.IDP.SP}_kidp-1.URI}_inv(KC)}_KSP			| Identity confirmation
 SP->C:{{Resource(URI)}_inv(SP)}_KC

 

LIMITATIONS:
The SSL channels are modeled using asymmetric keys. Thus, in principle, this model could yield spurious attacks.

 

PROBLEMS:
2

 

CLASSIFICATION:
G2 G12

 

ATTACKS:
None

 


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.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':=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.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))
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.SP)}_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()