B, M : agent PKb : public key SCm : text X : symmetric key (fresh)The object {\texttt{SCm}} denotes the secret certificate of the mobile M which is issued by a trusted central authority.1. B -> M : B, PKb 2. M -> B : {x}PKb 3. M -> B : {M, SCm}x
Upon receiving {\texttt{B}}'s public key {\texttt{PKb}}, the mobile uses it to encrypt the session key {\texttt{X}}, and sends the encrypted message to {\texttt{B}}. The mobile also sends its identity and secret certificate encrypted under {\texttt{X}} to authenticate {\texttt{X}} to the base. The encryption in message 3 is carried out using a symmetric key cryptosystem. Since this encryption is negligible compared to the public key encryption in message 2, the computational effort at the mobile is effectively reduced to that of modulo squaring of the session key.
i -> (b,3) : start (b,3) -> i : b,kb i -> (m,4) : b,ki (m,4) -> i : {x0(m,4)}ki,{m,scm1}x0(m,4)suffices (i) to violate the secrecy of the established session key {\texttt{X}} and (ii) to make the base station {\texttt{B}} to believe talking with the mobile {\texttt{M}} while it is talking with the intruder.
role msr_Base(B, M : agent, PKb : public_key, SCm : text, Snd, Rcv : channel(dy)) played_by B def= local State : nat, X : symmetric_key init State := 0 transition 1. State = 0 /\ Rcv(start) =|> State' := 1 /\ Snd(B.PKb) 2. State = 1 /\ Rcv({X'}_PKb.{M.SCm}_X') =|> State' := 2 /\ wrequest(B,M,x,X') end role
role msr_Mobile(B, M : agent, SCm : text, Snd, Rcv : channel (dy)) played_by M def= local State : nat, PKb : public_key, X : symmetric_key const secx : protocol_id init State := 0 transition 1. State = 0 /\ Rcv(B.PKb') =|> State' := 1 /\ X' := new() /\ Snd({X'}_PKb'.{M.SCm}_X') /\ witness(M,B,x,X') /\ secret(X',secx,{B,M}) end role
role session(B, M : agent, PKb : public_key, SCm : text) def= local SA, RA, SB, RB : channel (dy) const x : protocol_id composition msr_Base(B,M,PKb,SCm,SA,RA) /\ msr_Mobile(B,M,SCm,SB,RB) end role
role environment() def= const b,m : agent, kb, ki : public_key, scm1,scm2,scm3 : text intruder_knowledge = {b,m,scm2,scm3,i,ki,inv(ki)} composition session(b,m,kb,scm1) /\ session(b,i,kb,scm2) /\ session(i,m,ki,scm3) end role
goal % The established key X must be a secret between the base and the mobile secrecy_of secx % addresses G12 % Authentication: base station authenticates mobile %MSR_Base weakly authenticates MSR_Mobile on x weak_authentication_on x % addresses G1, G2 end goal
environment()