[Avispa-users] Why agent A use intruder's public key?

[m_barho at encs.concordia.ca]

Hello All

when i compiled the following example from AVISPA manual:


%A -> B: {Na.A}_Kb
%B -> A: {Nb.xor(Na,B)}_Ka
%A -> B: {Nb}_Kb

role alice (A,B : agent,
		Ka,Kb : public_key,
		Snd,Rcv : channel (dy)) played_by A def=
	local
		State : nat,
		Na : message,
		Nb : text
	init State := 0
	transition

	1. State = 0 /\ Rcv(start) =|>
		State':= 1 /\ Na' := new() /\ Snd({Na'.A}_Kb)
		/\ witness(A,B,bob_alice_na,Na')
		/\ secret(Na',na,{A,B})
	2. State = 1 /\ Rcv({Nb'.xor(Na,B)}_Ka) =|>
		State':= 2 /\ Snd({Nb'}_Kb)
		/\ wrequest (A,B,alice_bob_nb,Nb')
end role

%??????????????????????????????????????????

role bob (B,A : agent,
		Kb,Ka : public_key,
		Snd,Rcv : channel (dy)) played_by B def=
	local
		State : nat,
		Na : message,
		Nb : text
	init State := 0
	transition

	1. State = 0 /\ Rcv({Na'.A}_Kb) =|>
		State':= 1 /\ Nb' := new() /\ Snd({Nb'.xor(Na',B)}_Ka)
		/\ witness(B,A,alice_bob_nb,Nb')
		/\ secret(Nb',nb,{A,B})
	2. State = 1 /\ Rcv({Nb}_Kb) =|>
		State':= 2 /\ wrequest(B,A,bob_alice_na,Na)
end role

%??????????????????????????????????????????

role session (A,B: agent,
		Ka, Kb : public_key) def=
		local SA, RA, SB, RB: channel (dy)
	composition
		   alice(A,B,Ka,Kb,SA,RA)
		/\ bob(B,A,Kb,Ka,SB,RB)
end role

%??????????????????????????????????????????

role environment() def=
	const
		a, b, i : agent,
		ka, kb, ki : public_key,
		bob_alice_na,
		alice_bob_nb,
		na, nb : protocol_id

	intruder_knowledge = {a,b,i,ka,kb,ki,inv(ki)}

	composition
		session(a,b,ka,kb)
	     /\ session(a,i,ka,ki)
end role

%??????????????????????????????????????????

goal
	weak_authentication_on alice_bob_nb
	weak_authentication_on bob_alice_na
	secrecy_of na, nb
end goal

%??????????????????????????????????????????

environment()



it shows the following attack:

ATTACK TRACE
i -> (a,6): start
(a,6) -> i: {Na(1).a}_ki
i -> (b,3): {Na(1) XOR i XOR b.a}_kb
(b,3) -> i: {Nb(2).Na(1) XOR i}_ka
i -> (a,6): {Nb(2).Na(1) XOR i}_ka
(a,6) -> i: {Nb(2)}_ki
i -> (i,17): Nb(2)
i -> (i,17): Nb(2)

What i don't understand, why do agent A encrypts the first message  
using intruder's public key, while he wants to talk to B and he knows  
the B's public key?  Can anyone help?

Regards,
Malek