PROTOCOL:
SRP: Secure remote passwords

PURPOSE:
A client and a server authenticate each other based on
a password such that the password remains secret, even if it is guessable.  

REFERENCE:

 

MODELER:

 

ALICE_BOB:

We have a password p initially shared between the participants and a random number s, the salt (which at least the server knows initially). Original protocol, according to RFC:
 identifiers & macros:
 U =  
 p = 
 s =  (see notes section below)
 N = 
 x = SHA(s | SHA(U | ":" | p))
 v = g^x mod N, the "password verifier"
 a = 
 b =  
 A = g^a mod N
 B = v + g^b mod N
 u = H(A,B)
 S = (B - g^x) ^ (a + u * x) mod N 
   = (A * v^u) ^ b mod N
 K = SHA_Interleave(S)
 M = H(H(N) XOR H(g),H(U),s,A,B,K)
 -----------------------------------------------------------------
 Client -> Host   : U,A
 Host   -> Client : s,B
 Client -> Host   : M
 Host   -> Client : H(A,M,K)
 -----------------------------------------------------------------
 
Simplified version:
 Macros:
 K = H(V.(G^Na)^Nb)
 M = H(H(G),H(A).Salt.G^Na.{G^Nb}V.K)
 -----------------------------------------------------------------
 A -> B : A, G^Na
 B -> A : Salt, {G^Nb}V
 A -> B : M
 B -> A : H(G^Na,M,K)
 
 

PROBLEMS:
3
 

ATTACKS:
None
 

LIMITATIONS:

Note that the protocol is slightly simplified as in the original version a full-scale algebraic theory is required.  

NOTES:

A salt is a commonly-used mechanism to render dictionary (i.e. guessing) attacks more difficult. Standard UNIX password files, for instance, store a hash of each password prepended with a two-character salt. In this way, each possible password can map to 4096 different hash values, as there are 4096 possible values for the salt. This therefore greatly increases the computing power required for an intruder to mount a password guessing attack based on a precomputed dictionary of passwords and corresponding hash values.  


HLPSL:

role srp_Init (A,B : agent,
               Password : symmetric_key,
               H : hash_func,
               G : text,
               Snd,Rcv:channel(dy))
played_by A
def=

  local State : nat, 
        Na    :text,
        Salt  : protocol_id,
        DHY, V, K, M : message

  const sec_i_K : protocol_id

  init  State := 0

  transition

  1. State = 0  /\ Rcv(start) =|>
     State':= 1 /\ Na' := new()
                /\ Snd(A.exp(G,Na'))  

  2. State = 1  /\ Rcv(Salt'.{DHY'}_(exp(G,H(Salt'.H(A.Password))))) =|> 
     State':= 2 /\ V' := exp(G,H(Salt'.H(A.Password))) 
                /\ K' := H( V'.exp(DHY',Na) )
                /\ M' := H(H(G).H(A).Salt'.exp(G,Na).{DHY'}_V'.K' )
                /\ Snd( M' )
                /\ witness(A,B,k1,K')
                /\ secret(K',sec_i_K,{A,B})

  3. State = 2  /\ Rcv(H(exp(G,Na).M.K)) =|>  
     State':= 3
                /\ request(A,B,k2,K)

end role


role srp_Resp (B, A: agent, Password: symmetric_key, Salt: protocol_id, H: hash_func, G: text, Snd, Rcv:channel(dy)) played_by B def= local State : nat, Nb : text, M, K, DHX, V: message const sec_r_K : protocol_id init State := 0 transition 1. State = 0 /\ Rcv(A.DHX') =|> State':= 1 /\ Nb' := new() /\ Snd(Salt.{exp(G,Nb')}_(exp(G,H(Salt.H(A.Password))))) /\ V' := exp(G,H(Salt.H(A.Password))) /\ K' := H( V'.exp(DHX',Nb') ) /\ M' := H(H(G).H(A).Salt.DHX'.{exp(G,Nb')}_V'.K') /\ witness(B,A,k2,K') /\ secret(K',sec_r_K,{A,B}) 2. State = 1 /\ Rcv(M) =|> State':= 3 /\ Snd(H(DHX.M.K)) /\ request(B,A,k1,K) end role
role session(A,B: agent, Password: symmetric_key, Salt: protocol_id, H: hash_func, G: text) def= local SA,RA,SB,RB: channel (dy) composition srp_Init(A,B,Password,H,G,SA,RA) /\ srp_Resp(B,A,Password,Salt,H,G,SB,RB) end role
role environment() def= const k1,k2 : protocol_id, a,b,i: agent, kab,kai,kbi: symmetric_key, s_ab,s_ai,s_bi: protocol_id, h: hash_func, g: text intruder_knowledge = {i, kai, kbi, s_ai, s_bi} composition session(a,b,kab,s_ab,h,g) /\ session(a,i,kai,s_ai,h,g) /\ session(b,i,kbi,s_bi,h,g) end role
goal % confidentiality (G12) secrecy_of sec_i_K, sec_r_K % Entity Authentication (G1) % Message Authentication (G2) % Replay Protection (G3) --- forgotten in d6.1 authentication_on k2 authentication_on k1 end goal
environment()