PROTOCOL:
TSIG

PURPOSE:

This protocol allows for transaction level authentication using shared secrets and one way hashing. It can be used to authenticate dynamic updates as coming from an approved client, or to authenticate responses as coming from an approved recursive name server.  

REFERENCE:

[RFC2845]  

MODELER:

 

ALICE_BOB:

1. C -> S: TAG1.M1.{H(TAG1.M1).N1}_K
2. S -> C: TAG2.M1.M2.{H(TAG2.M1.M2).N2}_K

 

LIMITATIONS:

Since this protocol can be used to secure any transactions, we assume here that the constant {\tt M1} represents a request of a client and {\tt M2} is a response corresponding to the request. The variables {\tt N1} and {\tt N2} are two timestamps represented here by two nonces.

 

PROBLEMS:
2

 

CLASSIFICATION:
G1, G2

 

ATTACKS:
None

 

NOTES:
Client is the initiator. He sends a DNS request whose integrity
is ensured by {\tt \{H(M1).N1\}\_K} where {\tt K} is a shared secret. Server sends a DNS response whose integrity and freshness are ensured as well, by {\tt \{H(M1.M2).N2\}\_K}.  


HLPSL:


role client (A, S     : agent,
             K        : symmetric_key,
             H        : hash_func,
             M1       : text,
             Tag1,Tag2 :text,
             SND, RCV : channel(dy))
  played_by A def=

  local  State : nat,
         N1, N2, M2 : text
  init State:=0

  transition     
    step1. State=0
           /\  RCV(start) 
          =|> 
           State':=1 
           /\ N1':=new()
           /\ SND(Tag1.M1.{H(Tag1.M1).N1'}_K) 
           /\ witness(A,S,server_client_k_ab,Tag1.M1.{H(Tag1.M1).N1'}_K)


    step2. State=1
           /\ RCV(Tag2.M1.M2'.{H(Tag2.M1.M2').N2'}_K) 
          =|> 
           State':=2 
           /\ wrequest(A,S,client_server_k_ba,Tag2.M1.M2'.{H(Tag2.M1.M2').N2'}_K)
end role


role server(S : agent, A : agent, K : symmetric_key, H : hash_func, M2 : text, Tag1,Tag2: text, SND, RCV : channel(dy)) played_by S def= local State : nat, N1,M1,N2 : text init State:=0 transition step1. State=0 /\ RCV(Tag1.M1'.{H(Tag1.M1').N1'}_K) =|> State':=1 /\ N2':=new() /\ SND(Tag2.M1'.M2.{H(Tag2.M1'.M2).N2'}_K) /\ witness(S,A,client_server_k_ba,Tag2.M1'.M2.{H(Tag2.M1'.M2).N2'}_K) /\ wrequest(S,A,server_client_k_ab,Tag1.M1'.{H(Tag1.M1').N1'}_K) end role
role session(A,S : agent, K : symmetric_key, M1,M2 : text, H : hash_func, Tag1,Tag2 : text, Se,Re,Sf,Rf : channel(dy)) def= const server_client_k_ab, client_server_k_ba: protocol_id composition client(A,S,K,H,M1,Tag1,Tag2,Se,Re) /\ server(S,A,K,H,M2,Tag1,Tag2,Sf,Rf) end role
role environment() def= local Ra,Rs,Sa,Ss,Si,Ri : channel(dy) const a,s,i : agent, kia,kis,kas : symmetric_key, m1,m2,mi1,mi2,tag1,tag2 : text, h : hash_func intruder_knowledge = {i,a,s,h,kia,kis,mi1} composition session(a,s,kas,m1,m2,h,tag1,tag2,Sa,Ra,Ss,Rs) /\ session(a,s,kas,m1,m2,h,tag1,tag2,Sa,Ra,Ss,Rs) /\ session(i,s,kis,m1,m2,h,tag1,tag2,Si,Ri,Ss,Rs) /\ session(a,i,kia,m1,m2,h,tag1,tag2,Si,Ri,Ss,Rs) end role
goal weak_authentication_on server_client_k_ab % addresses G1,G2 weak_authentication_on client_server_k_ba % addresses G1,G2 end goal environment()