% @verbatim(Formalization of the Anonymous Shopping case study)
% @verbatim(IDMX Scene 3: Anonymous Bonus System.)
% @verbatim(In this specification a Wineshopper (Alice))
% @verbatim(purchases some goods from an online Winery)
% @verbatim(preventing to reveal to the Winery any unecessary)
% @verbatim(information about herself. In this scene the)
% @verbatim(Winery wants to apply a discount to a client)
% @verbatim(prooving the possession of 2 unique credentials,)
% @verbatim(in addition to the one needed to order some wine i.e.)
% @verbatim(a Passport credential as the one in Scene 1 and 2.)
% @verbatim(Each of the 2, one show, credential is called "stamp")
% @verbatim(and is obtained through previous purchases of goods)
% @verbatim(In this scene the Wineshopper makes 3 orders: the first)
% @verbatim(two to obtain stamps, and the last one with a)
% @verbatim(discount)
% @verbatim(%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%)
% @verbatim(Security requirements classification:)
% @verbatim(Privacy and One show credentials)
% @verbatim(Expected outcome of validation: NO_ATTACK_FOUND)
% @verbatim(For further details see Deliverables D5.{1,3})
% @modeler(Sebastian M{\"o}dersheim, IBM Research, 2009)
% @modeler(Marco Rocchetto, UniVr, 2010)
% @modeler(Alberto Calvi, UniVr, 2010)
% @satmc()
% @ofmc(--classic --untyped)
% @clatse(--nb 2 --untyped)
specification IDMXScene3_Safe channel_model CCM
entity Environment{
	import IDMXBase; 
	types
		order < message;
	symbols
		%% Partecipants
		ws,w,t,wcomp: agent;
		x1,x2,x3,x4: nat;
		Oecdgov: agent set;
		% wineshopper's passports values, 
		% used in Env body to set a credential
		% and then store it into Wineshoper's db
		NymIt: nym;
		val1,val2,val3: idmxval;
		val4,val: message;
		% db label for storing stamps
		stamps: message; 
		executabilityWS, executabilityW: fact;
		% fact symbol used to determine if a 
		% one-show credential has been spent
		% or not. If spent(Cred) holds, then 
		% Cred has been already used by its
		% owner
		noninvertible nonpublic spent(credential): fact;
		% fact symbol used to determine if the
		% Wineshopper has provided 2 already spent stamps.
		% (It never holds)
		noninvertible nonpublic fail(chPsy,credential,credential): fact;
		% fact symbol used to check if the protocol
		% has completed successfully
		noninvertible nonpublic discount(agent): fact;
	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	%% the Wineshopper entity (Alice)
	entity Wineshopper(Actor, Winery, Judge: agent){
		symbols 
		P: chPsy;
		Nym,NymI: nym;
		R_1,R_2: nat;
		C,VE,Other,Order:message;
		Surname,Prename,Dateofbirth: idmxval;
		Username:agent;
		Cred:message;
		I:agent;
		%% variables containing received stamps
		Stamp_1,Stamp_2: credential;       
		body{
			P := fresh();
			iknows(P);
			iknows(inv(P));
			% 1. Create Nym:
			%%%%%%%%%%%%%%%%
			R_1 := fresh();
			C := commit(masec_(Actor),Winery,R_1);
			[Actor]_[P] *-> Winery: spk((masec_(Actor).R_1),C,commitproof,Winery); 
			Winery ->* [Actor]_[P]: ?R_2;
			Nym := ptag(masec_(Actor),Winery,R_1,R_2);
			add(db(Actor),isnym.Nym.Winery);
			[Actor]_[P] *-> Winery: spk((masec_(Actor).R_1),Nym,ptagproof,Winery);
			% 2. Take a fitting passport:
			%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
			select {
				on (contains(db(Actor),cred.sign(inv(pk(?I)),
				credential(?I,?NymI,?Surname.?Prename.?Username.?Dateofbirth.?Other))) 
				): 
				{
				Cred := sign(inv(pk(I)),credential(I,NymI,Surname.Prename.Username.Dateofbirth.Other));
				VE := crypt(pk(Judge),Surname.Prename.Username.Dateofbirth);
				%% The Wineshopper orders 3 times: 
				%% - 1st and 2nd to order some good and receive two
				%%   different valid stamps
				%% - 3rd to order something and sending the 2 stamps
				%%   obtained before in order to get a discount
				%% First Order
				Order := fresh();
				add(db(Actor),ordered.Winery.Order);
				[Actor]_[P] *-> Winery: spk(Cred.masec_(Actor),VE,over18,Winery.Order.VE);
				Winery *->* [Actor]_[P]: ?Stamp_1;
				add(db(Actor),stamps.Winery.Stamp_1);
				%% Second order
				%% it could be done with a fresh new 
				%% IDMX Pseudonym but we have used the 
				%% old one in order to simplify
				%% the model (reducing the number of
				%% step transition in the translated 
				%% ASLan specification)
				Order := fresh();
				add(db(Actor),ordered.Winery.Order);
				[Actor]_[P] *-> Winery: spk(Cred.masec_(Actor),VE,over18,Winery.Order.VE);
				Winery *->* [Actor]_[P]: ?Stamp_2;
				add(db(Actor),stamps.Winery.Stamp_2);
				%% Third order, the one with discount
				Order := fresh();
				add(db(Actor),ordered.Winery.Order);
				[Actor]_[P] *-> Winery: spk(Cred.masec_(Actor).Stamp_1.Stamp_2,VE,over18,Winery.Order.VE);
				executabilityWS;
				} %%on closure
			} %% select closure
		}%body
	}%entity WineShopper
	entity Winery(Actor, Judge: agent, Oecdgov: agent set){
		symbols
			P:chPsy;
			Z_NymI,Nym: nym;
			VE,Order,Z_Birthdateval,Z_Other: message;
			R_2,Z_R_1: nat;
			Z_Masec: masec;
			Z_Surname,Z_Prename: idmxval;
			Z_Username:agent;
			I: agent;
			Cred: message;
			%% the stamp for the customer
			Stamp: credential; 	  
			% the 2 received Stamps that
			% need to be checked before 
			% granting the discount
			Stamp_1,Stamp_2: credential;
		body{
			% 1. Pseudonym
			%%%%%%%%%%%%%%
			[?]_[?P] *-> Actor: spk((?Z_Masec.?Z_R_1),commit(?Z_Masec,Actor,?Z_R_1),commitproof,Actor);
			R_2 := fresh();
			Actor ->* [?]_[P]: R_2;
			[?]_[P] *-> Actor: spk((Z_Masec.Z_R_1),ptag(Z_Masec,Actor,Z_R_1,R_2),ptagproof,Actor);
			Nym := ptag(Z_Masec,Actor,Z_R_1,R_2);
			add(db(Actor),isnym.Nym);
			% 2./3. Check spk and stuff
			%% this while cycle is executed 3 times
			while(!discount(P)){
				select{
				%% The Wineshopper is not in possession of enough stamp credentials
				%% first "on" branch
					on([?]_[P] *-> Actor:  
						spk(sign(inv(pk(?I)),credential(?I,?Z_NymI,?Z_Surname.?Z_Prename.?Z_Username.
						mkval(?Z_Birthdateval,one).?Z_Other)).Z_Masec,
						crypt(pk(Judge),?Z_Surname.?Z_Prename.?Z_Username.mkval(?Z_Birthdateval,one)),
						over18,
						Actor.?Order.crypt(pk(Judge),?Z_Surname.?Z_Prename.?Z_Username.mkval(?Z_Birthdateval,one))) 
					):
					{
						select{ on (contains(Oecdgov,I)) : 
							{
							Cred := sign(inv(pk(I)),credential(I,Z_NymI,Z_Surname.Z_Prename.Z_Username.
							mkval(Z_Birthdateval,one).Z_Other));
							VE := crypt(pk(Judge),Z_Surname.Z_Prename.Z_Username.mkval(Z_Birthdateval,one));
							add(db(Actor), ordered.spk(Cred.Z_Masec,VE,over18,Actor.Order.VE));
							Stamp := fresh();
							add(db(Actor), stamps.Z_Username.Stamp);
							Actor *->* [?]_[P]: Stamp;
							}
						}
					} %% end of the first on branch
				%% The Wineshopper prove to have stamp credentials
				%% second on branch
					on([?]_[P] *-> Actor: 
						spk(sign(inv(pk(?I)),credential(?I,?Z_NymI,?Z_Surname.?Z_Prename.?Z_Username.
						mkval(?Z_Birthdateval,one).?Z_Other)).Z_Masec.?Stamp_1.?Stamp_2,
						crypt(pk(Judge),?Z_Surname.?Z_Prename.?Z_Username.mkval(?Z_Birthdateval,one)),
						over18,
						Actor.?Order.crypt(pk(Judge),?Z_Surname.?Z_Prename.?Z_Username.
						mkval(?Z_Birthdateval,one))) 
					):
					{
						select{ on (contains(Oecdgov,I)) : 
							{
							Cred := sign(inv(pk(I)),credential(I,Z_NymI,Z_Surname.Z_Prename.Z_Username.
							mkval(Z_Birthdateval,one).Z_Other));
							VE := crypt(pk(Judge),Z_Surname.Z_Prename.Z_Username.mkval(Z_Birthdateval,one));
							%% The Winery checks if the stamps are usable or not
							if(!spent(Stamp_1) &  !spent(Stamp_2) &
							contains(db(Actor),stamps.Stamp_1) &
							contains(db(Actor),stamps.Stamp_2)
							){
								%% the received stamps are valid
								discount(P);
								add(db(Actor), ordered.spk(Cred.Z_Masec,VE,over18,Actor.Order.VE));
								spent(Stamp_1);
								spent(Stamp_2);
								executabilityW;
							}else {
								if(!contains(db(Actor), ordered.spk(Cred.Z_Masec,VE,over18,Actor.Order.VE)))
								{
									%% the received stams have been already used
									%% and it is not an old order (iknows facts are persistent)
									%% so we have to check that the second on branch
									%% has not been taken a second time because of
									%% an old iknows fact
									fail(P,Stamp_1,Stamp_2);
								}
							}
							} %% inner on branch closure
						} %% select closure
					} %% end of the second on branch
				} %% main select branch closure
			} %% while closure
		}%body
	}%entity Winery
	body{ %Environment
		NymIt := ptag(masec_(it),ws,x1,x2);
		%% We suppose that the Wineshopper has obtained a credential (passport) from Italy and
		%% has stored it in its db
		add(db(it),issued.NymIt.credential(it,NymIt,val1.val2.ws.mkval(val,one).val4));
		add(db(ws),cred.sign(inv(pk(it)),credential(it,NymIt,val1.val2.ws.mkval(val,one).val4))); 
		NymIt := ptag(masec_(it),i,x3,x4);
		add(db(it),issued.NymIt.credential(it,NymIt,val1.val2.i.mkval(val,one).val4));
		iknows(sign(inv(pk(it)),credential(it,NymIt,val1.val2.i.mkval(val,one).val4)));
		iknows(inv(ak(w)));
		iknows(inv(ck(w)));
		iknows(inv(pk(w)));
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		%% Instantiation of shoppers, wineries and 
		%% Judge (trusted third party)
		%% setting the Oecdgov members set
		Oecdgov := {aus,a,b,cdn,cz,dk,sf,f,d,gr,h,is,irl,it,j,kr,lu,
		mex,nl,nz,n,pl,p,sk,es,se,che,tr,uk,us};
		new Wineshopper(ws,w,t);
		new Winery(w,t,Oecdgov);
    }
	goals
	correct_presentation_of_credentials:
	[](
		forall Org I NymI Surname Prename Agent Birthdateval Other VE Order X1 X2 Stamp Stamp1.
		(contains(
			db(Org),
			ordered.spk(sign(inv(pk(I)),credential(I,ptag(masec_(I),Agent,X1,X2),Surname.
			Prename.Agent.mkval(Birthdateval,one).Other)).masec_(Agent),VE,over18,Org.Order.VE)
		)
		|
		contains(
			db(Org),
			ordered.spk(sign(inv(pk(I)),credential(I,ptag(masec_(I),Agent,X1,X2),Surname.
			Prename.Agent.mkval(Birthdateval,one).Other)).masec_(Agent).Stamp.Stamp1,VE,over18,Org.Order.VE)
		))
		=>
		contains(
			db(I),
			issued.ptag(masec_(I),Agent,X1,X2).credential(I,NymI,Surname.Prename.Agent.
			mkval(Birthdateval,one).Other)
		)
			&
		(
			( %% not(dishonest(Agent)) case
				contains(
					db(Agent),
					ordered.Org.Order
				)
			|
				%% dishonest(Agent) case
				%% since the intruder has received a legitimate
				%% credential ((s)he is an Italian citizen and is 
				%% at least 18 years old) we have to consider
				%% the possibility in which (s)he use that
				%% credential to order from a Winery
				%% But we can't be sure that (s)he will
				%% add the order to (her)his db
				dishonest(Agent)
			)
		) %% end of AND 
	); %% end of []
	intruder_knowledge_credential_masec:
	[](
		forall I Masec X1 X2 X3 Agent.
		iknows(credential(I,ptag(masec_(I),Agent,X1,X2),X3))
			=> 
		(
			dishonest(Agent)
			|
			dishonest(I)
		)
	);
	%% 2. Privacy: we only consider some secrecy properties for now.
	%% 2a. Nobody ever learns the master secret of an honest agent
	gdishonest: []( 
		forall Agent. 
		iknows(masec_(Agent)) 
			=>
		dishonest(Agent));
	%% 2b. Nobody ever learns other people's credentials or their values 
	nobody_learns_others_cred:
	forall Masec I X1 X2 X3 Agent.
	[](
		iknows(sign(inv(pk(I)), credential(I,ptag(masec_(I),Agent,X1,X2),X3))) &
		contains(Oecdgov,I)
		=>
		dishonest(Agent) 
		& 
		contains(db(I), issued.ptag(masec_(I),Agent,X1,X2).
		credential(I,ptag(masec_(I),Agent,X1,X2),X3))
	);
	% 4./5. Blind Signatures/One-Show Credentials
	one_show_creds_avoid_failure:
	forall Agent Stamp_1 Stamp_2 Org.
	[](
		discount(Agent)
			=>
		(
			(
			contains(db(Agent), stamps.Org.Stamp_1) &
			contains(db(Agent), stamps.Org.Stamp_2) 
			) 
			| 
			dishonest(Agent)
		)&
		contains(db(Org), stamps.Agent.Stamp_1) &
		contains(db(Org), stamps.Agent.Stamp_2) &
		!fail(Agent,Stamp_1,Stamp_2)
	);
}