auth_unlink.pv

set attacker = passive.
let system(appid:Appid,aaid:AAID,skAU:sskey,keyid:KeyID,wrapkey:key,token:bitstring,uname:Uname,facetid:Facetid,callerid:Callerid,cntr:CNTR) =
((* one RP authenticate one user many times *)
	(* write "let atype = autr_1b in" down to set the type you want to verify *)
	(* "autr_1b" for 1B,  "autr_1r" for 1R, "autr_2b" for 2B, "autr_2r" for 2R *)
	(* write "let ltype = empty in" down to set the phase you want to verify *)
	(* "empty" for first login, "stepup" for step-up authentication *)
	(* do not use the combination of autr_2b/autr_2r and empty *)
	let atype = autr_1b in
	let ltype = empty in 
	let pkAU = spk(skAU) in let testskAU = skAU in
	let kh = get_kh(atype,uname,appid,callerid,token,keyid,wrapkey,skAU) in
	let kid = get_kid(atype,kh,keyid) in
	let testkid = kid in
	insert ASMDB(appid,kid,kh);
	insert AutrDB(appid,kid,kh);
	out(c,(uname,appid,facetid,aaid,callerid,pkAU)); (* public info *)
	( 
		new https:channel; new CU:channel; new MC:channel; new AM:channel; out(c,https);
		new fakecallerid:Callerid; new fakefacetid:Facetid;
		new tr:Tr;
				(* following fields may leaked *)
				(*out(c,token);*)
				(*out(c,wrapkey);*)
				(*out(c,skAU);*)
				(*out(c,cntr);*)
				(*out(c,kid);*)
				(* there may exists following malicious entities *)
				(*AuthUA(https, c, uname, ltype)|*)
				(*AuthUC(c, MC, fakefacetid, ltype)|*)
				(*AuthUC(CU, c, facetid, ltype)|*)
				(*AuthUC(c, c, fakefacetid, ltype)|*)
				(*AuthASM(c,AM,token,fakecallerid,atype,ltype)|*)
				(*AuthASM(MC,c,token,callerid,atype,ltype)|*)
				(*AuthASM(c,c,token,fakecallerid,atype,ltype)|*)
				(*AuthAutr(c,aaid,wrapkey,cntr,tr,atype,ltype)|*)
		(* honest entities *)
		AuthRP(https, uname, appid, aaid,kid,pkAU,cntr,tr,ltype)|
		AuthUA(https, CU,uname, ltype)|
		AuthUC(CU, MC, facetid, ltype)|		
		AuthASM(MC,AM,token,callerid,atype,ltype)|		
		AuthAutr(AM,aaid,wrapkey,cntr,tr,atype,ltype)	
	)
).

process
(
	new appid:Appid;
	new aaid:AAID;
	new skAU:sskey; 
	new keyid:KeyID;
	new wrapkey:key;	
	new token:bitstring;	
	new uname:Uname;
	new cntr:CNTR;
	new facetid:Facetid; insert AuthAppList(appid,facetid);
	new callerid:Callerid; insert TrustCallerid(callerid);
	(* User 1 authenticates in RP 1 *)
	!system(appid,aaid,skAU,keyid,wrapkey,token,uname,facetid,callerid,cntr)|
	(* User 1 authenticates in RP 2 *)
	!(
		new appid2:Appid;
		new skAU2:sskey;
		new keyid2:KeyID;
		new wrapkey2:key;
		new token2:bitstring;
		new uname2:Uname;
		new cntr2:CNTR;
		system(appid2,aaid,skAU2,keyid2,choice[wrapkey2,wrapkey],choice[token,token2],uname2,facetid,callerid,cntr2)
	)
)