% @verbatim(Formalization of the Anonymous Shopping case study)
% @verbatim(IDMX Scene 1: Anonymous yet accountable shopping.)
% @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 complains for a missing payment with)
% @verbatim(a trusted third party modeled by Judge entity)
% @verbatim(in order to obtains the real Alice's Name and Surname.)
% @verbatim(%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%)
% @verbatim(Security requirements classification:)
% @verbatim(Privacy and Accountability)
% @verbatim(Expected outcome of validation: NO_ATTACK_FOUND)
% @verbatim(For further details see Deliverables D5.{1,2,3})
% @modeler(Sebastian M{\"o}dersheim, IBM Research, 2009)
% @modeler(Marco Rocchetto, UniVr, 2010)
% @modeler(Alberto Calvi, UniVr, 2010)
% @satmc()
% @ofmc(--classic --untyped)
% @clatse()
specification IDMXScene1_Safe channel_model CCM
entity Environment{
	import IDMXBase; 
	types
		order < message;
	symbols
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		%% Constant\Variable symbols
		%% for initializations
		%% Agents names 
		%% ws: Wineshopper (Alice)
		%% w: online Winery
		%% t: the trusted third party (Judge)
		ws,w,t: agent;
		%% the wine order made by Wineshopper
		o: order;		
		%% Wineshopper's passports values, 
		%% used in Env body to set a credential,
		%% store it into Wineshoper's db
		%% and then keeping trace of its
		%% issuing in the issuer db 
		NymIt: nym;
		val1,val2: idmxval;
		val4,val: message;
		%% some costant symbols for 
		%% credentials and Nyms initialization
		x1,x2,x3,x4: nat;
		%% Oecdgov set used in the body section
		Oecdgov: agent set;
		%% facts used to check the executability
		%% of the model (in *_execTrace.aslan++ files)
		executabilityJ,executabilityW,executabilityC,executabilityWS: fact;
	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	%% the Wineshopper entity (Alice)
	entity Wineshopper(Actor, Winery, Judge: agent, Order: message, Oecdgov: agent set){
		symbols 
			%% Variables declaration
			%% Channel Psudonym
			P: chPsy;
			%% Random numbers for the IDMX pseudonym
			R_1,R_2: nat;
			%% Actor's (Wineshopper's) and credential issuer's IDMX Pseudonyms
			Nym,NymI: nym;
			%% IDMX values and other information for
			%% proofs and commitments
			C,VE,Other: message;
			Surname,Prename,Dateofbirth: idmxval;
			Username: agent;
			%% the agent issuer of the credential
			I: agent;
		body{
 			P := fresh();
			iknows(P);
			iknows(inv(pk(P)));
			iknows(pk(P));
			% 1. Pseudonym (Nym) creation
			%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
			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)))):
				{
					% 3. Construct verifiable encryption:
					%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
					VE := crypt(pk(Judge),Surname.Prename.Username.Dateofbirth);
					% Transmission of all proofs and order:
					%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
					[Actor]_[P] *-> Winery: spk(sign(inv(pk(I)),credential(I,NymI,Surname.Prename.Username.
					Dateofbirth.Other)).masec_(Actor),VE,over18,Winery.Order.VE);
					add(db(Actor),ordered.Winery.Order);
					executabilityWS;
				}  
			} %% select closure
		} %% body closure
	} %% end of Wineshopper entity
	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	%% the online Winery entity
	entity Winery(Actor, Judge: agent, Oecdgov: agent set){
		symbols 
			%% Variables declaration
			%% Channel Psudonym of Wineshopper
			P: chPsy;
			%% Random numbers for the Whinesopper's IDMX pseudonym
			Z_R_1,R_2: nat;
			%% Actor's (Wineshopper's) and credential issuer's IDMX Pseudonyms
			Z_NymI,Nym: nym;
			%% IDMX values and other information for
			%% proofs and commitments
			Z_Masec: masec;
			VE,Order,Z_Birthdateval,Z_Other: message;
			Z_Surname,Z_Prename: idmxval;
			Z_Username: agent;
			%% variable to store the signed credential
			Cred: message;
			%% the agent issuer of the credential
			I: agent;			
		body{
			% 1. Pseudonym (Nym) creation
			%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
			[?]_[?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. The Winery receives the proof and checks it
			%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
			[?]_[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))
				);
			%% checking if agent I is member of the Oecdgov
			select{ on (contains(Oecdgov,I)) : 
				{
				%% if it is the case, the Winery stores the Credential and the order
				%% information (along with encrypted Wineshopper's data (VE) that the Judge can decrypt)
				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));
				executabilityW;
				}
			} %% select closure
		} %% body closure
	} %% end of Winery entity
	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	%% the online Winery entity can also
	%% complain (play the role of
	%% "WineryComplain") in the case 
	%% of a missing payment from the 
	%% Wineshopper (modeled only in Scene 1)
	entity WineryComplain(Actor,Judge: agent, Order: message){
		symbols
			%% Variables declaration
			%% Order data sended to the Jusdge
			Z_Credential,VE: message;
			Z_Masec: masec;
		body{
			select{ on(contains(db(Actor),ordered.
				spk(?Z_Credential.?Z_Masec,?VE,over18,Actor.Order.?VE))):
				{
				%% sending the complaint to the Judge
				Actor -> Judge: spk(Z_Credential.Z_Masec,VE,over18,Actor.Order.VE);
				executabilityC;
				}
			}
		} %% body closure
	} %% end of entity WineryComplain (role played by the Winery)
	%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
	%% the Judge entity 
	entity Judge(Actor,Shop: agent){
		symbols
			%% Variables declaration
			Z_Credential: message;
			VE,Order,Birthdateval,Z_Other: message;
			Z_Masec: masec;
			Surname,Prename: idmxval;
			Username: agent;
			I: agent;
			Z_NymI: nym;
		body{
			%% Waiting for a complaint
			Shop -> Actor: spk(?Z_Credential.?Z_Masec,?VE,over18,Shop.?Order.?VE);
			%% Storing it in the database
			add(db(Actor), complaint.Shop.spk(Z_Credential.Z_Masec,VE,over18,Shop.Order.VE));
			%% checking all fields
			select{on((Z_Credential=sign(inv(pk(?I)),credential(?I,?Z_NymI,?Surname.?Prename.?Username.
						mkval(?Birthdateval,one).?Z_Other))
				& VE = crypt(pk(Actor),	?Surname.?Prename.?Username.mkval(?Birthdateval,one)))):
				{
					%% breaking anonymity and storing in the db
					add(db(Actor),opened.Order.Surname.Prename.Username.mkval(Birthdateval,one).Shop);
					%% introducing "executability" fact to test
					%% the executability of the whole protocol
					executabilityJ;
				}
			}
		} %% body closure
	} %% end of entity Judge
	%% Formalizing the body of the Environment entity
	body{ 
		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(ws),cred.sign(inv(pk(it)),credential(it,NymIt,val1.val2.ws.mkval(val,one).val4))); 
		%% So Italy (agent "it") keeps trace of the issued credential
		add(db(it),issued.NymIt.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(iOrder);		
		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
		%% 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};
		%% Whineshopper and Winery instantiation
		new Wineshopper(ws,w,t,o,Oecdgov);
		new Winery(w,t,Oecdgov);
		%% WineryComplain instantiation
		%% note that this role is played 
		%% by the same agent who has 
		%% played the Winery, namely "w"
		new WineryComplain(w,t,o); 
		%% Judge instantiation
		%% it is aware of the name of the 
		%% agent playing the role "Winery" 
		%% (and thus "WineryComplain")
		new Judge(t,w);
	} %% body closure
	goals
	%% 1. Correct presentation of credentials
	%% (a) If the org accepts an order, then the order was given that
	%% way by an honest or dishonest user:
	correct_presentation_of_credentials:
	[](
		forall Org I NymI Surname Prename Agent Birthdateval Other VE Order X1 X2.
		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(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 []
	%% (b) if the judge reveals the identity of a user who has ordered
	%% then this user has indeed ordered
	really_ordered:
	[](
		forall Judge Order Surname Prename Agent Birthdateval Shop I NymI X1 X2 X3 Other.    
		contains(db(Judge),opened.Order.Surname.Prename.Agent.mkval(Birthdateval,one).Shop)
			=>
		(
			( %% not(dishonest(Agent)) case
				contains(db(Agent),ordered.Shop.Order)
				& 
				contains(db(Agent),cred.sign(inv(pk(I)),
				credential(I,NymI,Surname.Prename.Agent.mkval(Birthdateval,one).Other)))
				&
				contains(db(I),issued.ptag(masec_(I),Agent,X1,X2).
				sign(inv(pk(I)),credential(I,ptag(masec_(I),Agent,X1,X2),X3)))
			)
		| 
			( %% dishonest(Agent) case
			dishonest(Agent)
			)
		)
	);
	%% (c) when the intruder knows a credential, then he knows the master secret
	%% it is bound to:
	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 
	%% (in this scene).
	nobody_learns_others_cred:
	forall 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))
	);
	%% 3. Accountability
	%% If shop has an order with payment timeout, then Judge can find out
	%% the real name:
	judge_accountability:
	[](
		forall Org I NymI Surname Prename Agent Birthdateval Other Judge Shop Order Masec.
		contains(db(Judge),opened.Order.Surname.Prename.Agent.mkval(Birthdateval,one).Shop)
		=>
		( %% not(dishonest(Agent))
			contains(
				db(Org),
				ordered.spk(
					sign(inv(pk(I)),
					credential(
						I,NymI,Surname.Prename.Agent.mkval(Birthdateval,one).Other
					)).Masec,
					crypt(pk(Judge),Surname.Prename.Agent.mkval(Birthdateval,one)) ,
					over18,
					Org.Order.crypt(pk(Judge),Surname.Prename.Agent.mkval(Birthdateval,one)) 
				)
			) 
				&
			contains(
				db(Judge),
				complaint.Org.spk(
					sign(inv(pk(I)),credential(I,NymI,Surname.Prename.Agent.mkval(Birthdateval,one).Other
					)).Masec,
					crypt(pk(Judge),Surname.Prename.Agent.mkval(Birthdateval,one)),
					over18,
					Org.Order.crypt(pk(Judge),Surname.Prename.Agent.mkval(Birthdateval,one)) 
				)
			)
			&
			contains(Oecdgov,I)
		)
		|
		dishonest(Agent)
	);
	% 4./5. Blind Signatures/One-Show Credentials are not applicable
	% in this scene.
} %% end of Environment entity