[prev in list] [next in list] [prev in thread] [next in thread] 

List:       avispa-users
Subject:    Re: [Avispa-users] Very simple (partial) protocol doesn't work
From:       "Matteo R." <matteo.it () gmail ! com>
Date:       2011-04-05 7:56:07
Message-ID: 4D9ACB17.4080209 () gmail ! com
[Download RAW message or body]

Hello,
yesterday evening I had got some problems with the emails.
Anyway now I've instantiated all variables (as you've said me yesterday) 
but the protocol doesn't work at all.
The problem is still the second pass, that is not showed in SPAN.

What do you think? As usual, I attach the specification

Thank you very much
Matteo

["problem with partial protocol_3.txt" (text/plain)]

	
role roleA (

	Pr, Pe, PrM: agent,
	Hash: hash_func,
	K11: symmetric_key,		
	K2: symmetric_key,		
	SND_Pe, RCV_Pe, SND_PrM, RCV_PrM: channel(dy)
	)
	
	played_by Pr
	
	def=
	
	local
		State: nat
		
	const
		idPayer: protocol_id

		
	init
		State := 3
		
	transition
	
	

	
	end role						
								
	
role roleB (

	Pe, Pr, PeM: agent,
	Hash: hash_func,
	K12: symmetric_key,		
	K2: symmetric_key,	
	SND_Pr, RCV_Pr, SND_PeM, RCV_PeM: channel(dy)
	)
	
	played_by Pe
	
	def=
	
	local
		State: nat
		
	const
		idPayee: protocol_id

		
	init
		State := 3
		
	transition
		


		
		
	end role
	
	
role roleC (

	PrM, Pr, PeM, TSC: agent, 
	Hash: hash_func,
	K11: symmetric_key,			
	KMM: symmetric_key,			
	KeyRing1: (symmetric_key) set,		
	SND_Pr, RCV_Pr, SND_PeM, RCV_PeM, SND_TSC, RCV_TSC: channel(dy)
	)
	
	played_by PrM
	
	def=
	
	local
		State: nat,
		X1, X2: symmetric_key,		
		R: text,	
		NONCE: nat,	
		IDPe: hash(nat.nat),
		TID: text,	
		IDMno: text,		
		AMOUNT, DATE, DESC: text,		
		GeneralParams: (hash(nat.nat).text.text.text.text.text.nat), 	
		SecuredParams: {text.text}_symmetric_key,		
		SecuredGeneralParams: {text.text.text.text}_symmetric_key,	
		IDPr: hash(nat.nat),
		PNPr: nat,
		PINPr: nat,
		AIPr: nat,
		Timestamp1: nat
	
	const
		idPayer: protocol_id

		
	
	init
		State := 4
		
	transition
	


		11. State = 4 /\ RCV_Pr(start) =|>
		   State':=5  /\ IDPe':= new()
			      /\ IDMno':= new()
			      /\ R':= new()
			      /\ TID':= new()
			      /\ AMOUNT':= new()
			      /\ DATE':= new()
			      /\ NONCE':= new()
			      /\ GeneralParams':= (IDPe'.IDMno'.R'.TID'.AMOUNT'.DATE'.NONCE')
			      /\ SecuredParams':= new()
			      /\ X1':= new()
			      /\ IDPr':= new()
			      /\ SND_TSC(Hash({GeneralParams'.Hash(GeneralParams').SecuredParams'}_X1'.1.IDPr'))


		
		13. State = 5 /\ RCV_TSC(Timestamp1') =|>
		    State':=7 
			
		   
		   
		   
		   
end role

role roleD (

	PeM, Pe, PrM, TSC: agent, 
	Hash: hash_func,
	K12: symmetric_key,
	KMM: symmetric_key,			
	KeyRing2: (symmetric_key) set,		
	SND_Pe, RCV_Pe, SND_PrM, RCV_PrM, SND_TSC, RCV_TSC: channel(dy)
	)
	
	played_by PeM
	
	def=
	
	local
		State: nat

	const
		idPayee: protocol_id
	
	init
		State := 4
		
	transition
			 	    		     
		   	    
				
 
end role


role timeStamper (
	
	TSC, PrM, PeM: agent,
	Hash: hash_func,
	SND_PrM, RCV_PrM, SND_PeM, RCV_PeM: channel(dy)
	)
	
	played_by TSC
	
	def=
	
	local
		State: nat,
		GeneralParams: (hash(nat.nat).text.text.text.text.text.nat),
		SecuredParams: {text.text}_symmetric_key,			
		PartialGeneralParams: (text.text.text.text),		
		SecuredGeneralParams: {text.text.text.text}_symmetric_key,	
		SecuredKey: hash(symmetric_key),
		Yes_no: text,
		IDPr: hash(nat.nat),
		X1, Y2: symmetric_key,
		R: text,	
		NONCE: nat,
		IDPe: hash(nat.nat),
		TID: text,	
		IDMno: text,		
		AMOUNT, DATE, DESC: text,
		Timestamp1, Timestamp2: nat
		
	const
		idTimeStamper: protocol_id
		
	init
		State := 0
		
	transition
		

		
			12. State = 0 /\ RCV_PrM(Hash({GeneralParams'.Hash(GeneralParams').SecuredParams'}_X1'.1.IDPr')) \
=|>  State':=2 
						  /\ Timestamp1':= new()
						  /\ SND_PrM(Timestamp1')
		   	     
		   	     		   	

end role


role session (

	Pe, Pr, PeM, PrM, TSC: agent,
	Hash: hash_func,
	K11, K12, K2, KMM: symmetric_key
	)
	
	def=
	
	local
		SPr_Pe, RPr_Pe, SPr_PrM, RPr_PrM,
		SPe_Pr, RPe_Pr, SPe_PeM, RPe_PeM,
		SPrM_Pr, RPrM_Pr, SPrM_PeM, RPrM_PeM, SPrM_TSC, RPrM_TSC,
		SPeM_Pe, RPeM_Pe, SPeM_PrM, RPeM_PrM, SPeM_TSC, RPeM_TSC, 
		STSC_PrM, RTSC_PrM, STSC_PeM, RTSC_PeM: channel(dy),
			
		
		KeyRing1, KeyRing2: (symmetric_key) set,
		Success_failed: text,
		IDPe: hash(nat.nat),
		PNPe: nat,
		PINPe: nat,
		AIPe: nat,
		IDPr: hash(nat.nat),
		PNPr: nat,
		PINPr: nat,
		AIPr: nat
	
	composition			
	
		   roleA(Pr, Pe, PrM, Hash, K11, K2, SPr_Pe, RPr_Pe, SPr_PrM, RPr_PrM)
		/\ roleC(PrM, Pr, PeM, TSC, Hash, K11, KMM, KeyRing1, SPrM_Pr, RPrM_Pr, SPrM_PeM, \
RPrM_PeM, SPrM_TSC, RPrM_TSC)   /\ timeStamper(TSC, PrM, PeM, Hash, STSC_PrM, \
RTSC_PrM, STSC_PeM, RTSC_PeM)  /\ roleD(PeM, Pe, PrM, TSC, Hash, K12, KMM, KeyRing2, \
SPeM_Pe, RPeM_Pe, SPeM_PrM, RPeM_PrM, SPeM_TSC, RPeM_TSC)   /\ roleB(Pe, Pr, PeM, \
Hash, K12, K2, SPe_Pr, RPe_Pr, SPe_PeM, RPe_PeM)  
		
	end role
	
role environment()
	
	def=
	
	const
		pe, pr, tsc, peM, prM: agent,
		h: hash_func,
		success_failed: text,
		iDPe: message,
		iDPr: message,
		pNPe: nat,
		pINPe: nat,
		aIPe: nat,
		pNPr: nat,
		pINPr: nat,
		aIPr: nat,
		x1, x2, y1, y2, k11, k12, k2, kmm: symmetric_key
		
	intruder_knowledge = {i, pe, pr, tsc, peM, prM}  	
							
	composition	
		
		session(pe, pr, tsc, peM, prM, h, k11, k12, k2, kmm)
	%	/\ session(pe, i, peM, prM, h)
	%	/\ session(i, pr, peM, prM, h)
		
end role



environment()                



_______________________________________________
Avispa-users mailing list
Avispa-users@avispa-project.org
http://mail63.csoft.net/mailman/listinfo/avispa-users


[prev in list] [next in list] [prev in thread] [next in thread]