[Avispa-users] New specification is detect replay attack

[Adam Noureddine]

Dear friends, 

for this protocol:

1. A --- > B : na                      
2. B --- > A : {na}_K          

K is shared key between A and B
 

The change of specification of this protocol in HLPSL is:
     role server ( A,B: agent, K: symmetric_key, Snd,Rec: channel(dy))
    played_by A
    def=
      local  State         : nat,
              Na            : text    
            init State := 0 
      transition
       1. State = 0
          /\ Rec(start) 
          =|> 
          State' := 1
          /\ Na' := new()
 
          /\ Snd(Na')
   /\ witness(A,B,auth_client,Na')    
       2. State = 1
          /\ Rec({Na}_K)
          =|> 
          State' := 2
          /\ request(A,B,auth_client,Na)         
    end role

    role client ( B,A: agent,K: symmetric_key, Snd, Rec: channel(dy))
    played_by B
    def=
      local  State               : nat,
            
 Na                  : text          
      init State := 0
      transition
       1. State = 0
          /\ Rec(Na') 
          =|>
          State' := 1
          /\ Snd({Na'}_K)          
       
    end role

   role session(A,B : agent,K : symmetric_key)
def=
local St,Rt,Sl,Rl : channel(dy) 
composition
client(B,A,K,St,Rt)
/\ server(A,B,K,Sl,Rl)
end
 role

role environment() def=
const a,b,i : agent,
k : symmetric_key,
auth_client:protocol_id

intruder_knowledge = {a,b,k1,k2}

composition
session(a,b,k)
/\ session(i,b,k1)
/\ session(a,i,k2)

end role

    goal
     %  server authenticates client 
       authentication_on auth_client
    end goal
    environment()
---------------------------------------------------------------

After verification with AVISPA tools, the resultat is detect replay attack such as:

% OFMC
% Version of 2006/02/13
SUMMARY
  UNSAFE
DETAILS
  ATTACK_FOUND
PROTOCOL
  /home/avispa/web-interface-computation/./tempdir/workfileDubQFA.if
GOAL
  authentication_on_auth_client
BACKEND
  OFMC
COMMENTS
STATISTICS
  parseTime: 0.00s
  searchTime: 0.01s
  visitedNodes: 9 nodes
  depth: 2 plies
ATTACK TRACE
i -> (a,3): start
(a,3) -> i: Na(1)
i -> (b,3): Na(1)
(b,3) -> i: {Na(1)}_k
i -> (a,3): {Na(1)}_k


My question,My new specification is it correct ?


I’ am waiting your answer.
My best regards


      
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mail63.csoft.net/pipermail/avispa-users/attachments/20090827/7814a9d8/attachment-0001.htm