% @verbatim(Formalization of the Anonymous Shopping case study)
% @verbatim(IDMX Base file: common types, symbols and intruder)
% @verbatim(deduction rules used throughout IDMX scenes.)
% @modeler(Sebastian M{\"o}dersheim, IBM Research, 2009)
% @modeler(Marco Rocchetto, UniVr, 2010)
% @modeler(Alberto Calvi, UniVr, 2010)
% @satmc()
% @ofmc(--classic --untyped)
% @clatse()
%% Idemix Base: types, symbols and intruder deduction rules used throughout IDMX.
entity IDMXBase{
	types 
		chPsy     < public_key;    %% Psydonyms for pseudonymous secure channels 
		masec     < message;  %% IDMX Master secrets
		nym       < message;  %% IDMX pseudonyms
		proof     < message;  %% Zero-knowledge proofs
		credential< message;  %% IDMX credential
		statement < message;  %% Identifiers for proof statements
		idmxval   < message;  %% Special type for values in credential attributes 
	symbols
		%% function symbols
		nonpublic noninvertible masec_(agent):masec;  
			%% the master secret of a user
		noninvertible spk(message,message,statement,message):proof;
			%% signed non-interactive zero-knowledge proof:
			%% arguments: concatenation of secret values, 
			%%            concatenation public values, 
			%%            identifier for the proven statement 
			%%            message that is signed by the proof. 
		noninvertible commit(masec,agent,nat):message;
			%% commitment function 
		noninvertible ptag(masec,agent,nat,nat): nym; 
			%% constructor for IDMX pseudonyms 
			%% arguments: master secret of the user owning the pseudonym
			%%            name of the server at which the pseudonym is used 
			%%            random numbers by user and server
		mkval(message,message):idmxval;
			%% "constructor" for IDMX values, idea: carries abstraction of the 
			%% relation symbols that hold for it. This function cannot be 
			%% applied by any agent/intruder.
		credential(agent,nym,message):credential;
		db(agent):message set; 
			%% an agent's data base
		noninvertible blind(masec,idmxval): idmxval; 
			%% a blinding function used in scene 2
		noninvertible unblind(message,idmxval): idmxval; 
			%% an unblinding function
		%% costants symbols
		zero,one: message;    
			% used to replace character '0' and '1' resp. used as arguments in mkval function
		isnym,opened,ordered,cred,credp,credFcs,issued,complaint: message; 
			%% labels (or tables names) for agents' data bases
		commitproof,ptagproof,applicationproof,over18,proper : statement;
			%% identifiers for proven statement
		%% OECDGOV states members:
		%% Australia,Austria,Belgium,Canada,Czech Republic,Denmark,Finland,France,Germany,
		%% Greece,Hungary,Iceland,Ireland,Italy,Japan
		aus,a,b,cdn,cz,dk,sf,f,d,gr,h,is,irl,it,j: agent;
		%% Korea,Luxembourg,Mexico,Netherlands,New Zealand,Norway,Poland,Portugal,
		%% Slovak Republic,Spain,Sweden,Switzerland,Turkey,United Kingdom
		kr,lu,mex,nl,nz,n,pl,p,sk,es,se,che,tr,uk,us: agent;
		%% Fact symbol used for executability tests
		executability,executability1,executability2,executability3,executability4: fact;
	clauses
		%% intruder deduction rules for the defined function symbols
		%% which are not automatically generated by the ASLan++ Connector
		%% because they are custom deduction rules (i.e. they are not 
		%% Horn clauses about publicity nor fully invertibility of function
		%% symbols)
		iSeeDisMasec(A): iknows(masec_(A)) :- dishonest(A);
			%% The intruder knows the master secret of all dishonest agents
			%% masec_ is "partially public"
		noSecretFromProof_1(SEC,PUB,ST,MSG): iknows(PUB) :- iknows(spk(SEC,PUB,ST,MSG));
			%% From a zero-knowledge proof one can see everything but the
			%% secret values
		noSecretFromProof_2(SEC,PUB,ST,MSG): iknows(ST) :- iknows(spk(SEC,PUB,ST,MSG));
			%% From a zero-knowledge proof one can see everything but the
			%% secret values
		noSecretFromProof_3(SEC,PUB,ST,MSG): iknows(MSG) :- iknows(spk(SEC,PUB,ST,MSG));
			%% From a zero-knowledge proof one can see everything but the
			%% secret values
		noSecFromCommit_1(SEC,A,N1): iknows(A) :- iknows(commit(SEC,A,N1));
			%% From a commitment one can see everything but the
			%% secret values
		noSecFromCommit_2(SEC,A,N1): iknows(N1) :- iknows(commit(SEC,A,N1));
			%% From a commitment one can see everything but the
			%% secret values
		noSecretFromPtag_1(SEC,A,N1,N2): iknows(A) :- iknows(ptag(SEC,A,N1,N2));
			%% From a IDMX pseudonyms constructor one can see everything but the
			%% secret values
		noSecretFromPtag_2(SEC,A,N1,N2): iknows(N1) :- iknows(ptag(SEC,A,N1,N2));
			%% From a IDMX pseudonyms constructor one can see everything but the
			%% secret values
		noSecretFromPtag_3(SEC,A,N1,N2): iknows(N2) :- iknows(ptag(SEC,A,N1,N2));
			%% From a IDMX pseudonyms constructor one can see everything but the
			%% secret values
		iUnblind(S1,S2): iknows(S1) :- iknows(blind(S2,S1)) & iknows(S2);
			%% one can see a blinded value S1, only if (s)he already knows
			%% also the value used to blind it (S2)
}