(*************************************************************
 *                                                           *
 *       Unbound DNS resolver verifier								 *
 *                                                           *
 *       Samuel Son and Vitaly Shmatikov							 *
 *                                                           *
 *                                                           *
 *************************************************************)

param redundantHypElim = beginOnly.
param traceDisplay = long.
param traceBacktracking = false.

fun NSt/0. fun At/0. fun CNAMEt/0.
fun zeroStage/0.
fun oneStage/0.

fun ansChID/0.
fun authChID/0.
fun addChID/0.

data ValidIP/1.
data InvalidIP/1.
data ValidDN/1.
data InvalidDN/1.
data AA/1.

data nil/0.
data Record/3.

reduc GetSrc    ( Record( dmnSrc, target, recType ) ) = dmnSrc.
reduc GetDst    ( Record( dmnSrc, target, recType ) ) = target.
reduc GetType    ( Record( dmnSrc, target, recType ) ) = recType.
reduc GetDnDst  ( Record( dmnSrc, ValidDN(target), recType ) ) = target.

data Response/4.
reduc GetAnswer   ( Response( q1, Record(a1,a2,a3), Record(au1,au2,NSt), Record(ad1,ad2,At) ) ) 
						= Record(a1,a2,a3).
reduc GetAuth     ( Response( q1, Record(a1,a2,a3), Record(au1,au2,NSt), Record(ad1,ad2,At) ) ) 
						= Record(au1,au2,NSt).
reduc GetAdd      ( Response( q1, Record(a1,a2,a3), Record(au1,au2,Nst), Record(ad1,ad2,At) ) ) 
						= Record(ad1,ad2,At).

(* Channels *)
free net.
data emptyset/0.

(* Predicate checking whether it is valid or not *)
pred checkrec/1.
clauses
  checkrec: Record( x, InvalidIP(ip), At );
  checkrec: Record( x, InvalidDN(dn), NSt );
  checkrec: Record( x, InvalidDN(dn), CNAMEt ).

pred isInvalid/1.
clauses
  isInvalid:InvalidIP(ip);
  isInvalid:InvalidDN(dn).

data zero/0.
data succ/1.

pred geq/2.
clauses
	geq:x,x;
	geq:x,y -> geq:succ(x),y.

pred ga/2.
clauses
	ga:succ(x),x;
	ga:x,y -> ga:succ(x),y.

data true/0.

data mkName/1.
data seedRoot/0.
data dnmSeed/0.
data dnmIP/0.

data ERRORID0/0.
data ERRORID1/0.
data ERRORID2/0.
data ERRORID3/0.
data ERRORID4/0.
data ERRORID5/0.
data ERRORID6/0.
data ERRORID7/0.
data ERRORID8/0.
data ERRORID9/0.
data AAFLAG/0.
data EXIST/0.
data NONEXIST/0.

data makeSubName/2.
pred isSubName/2.
clauses 
  isSubName: x, x;
  isSubName: makeSubName( z, x ), x;
  isSubName: x, y -> isSubName: makeSubName( z, x ), y.	  

(* Non-overwritabilities in Section 6.3 for A *)
(* query ev: evPoison( At, cached_src_a, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ) 
	  ==> ev: evInitCache( Record( cached_src_a, cached_dst_a, At), lva ) & ga: lva, lv. 
  ( TRUE: in case, v6,v4 is true, FALSE: in case: v3{E7,E8-1,E9-1},v2{E7,E8,E9} ) 
*)

(* Non-overwritabilities in Section 6.3 for CNAME *)
(*	query ev: evPoison( CNAMEt, cached_src_cname, dst, lv, 
							cached_src_ns, cached_src_a, cached_src_cname, eid ).
	(Impossible in every case)
*)

(* Properties in Section 6.4 *)
(* query ev: evPoison( NSt, x, dst, lv, cached_src_ns,
					cached_src_a, cached_src_cname, eid ) ==> 
      ev: recursiveQueryStart( y, zone, zone_target ) 
      	& isSubName: x, zone & isSubName: y, zone.

	query ev: evPoison( At, x, dst, lv, cached_src_ns,
					cached_src_a, cached_src_cname, eid ) ==> 
      ev: recursiveQueryStart( y, zone, zone_target ) 
      	& isSubName: x, zone & isSubName: y, zone.

	query ev: evPoison( CNAMEt, x, dst, lv, cached_src_ns,
					cached_src_a, cached_src_cname, eid ) ==> 
      ev: recursiveQueryStart( y, zone, zone_target ) 
      	& isSubName: x, zone & isSubName: y, zone.
*)

(* Properties in Section 7.1 *) 
(*  query ev: evPoison( CNAMEt, x, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ) 
	  ==>	ev: evInitCache( Record( target, validIP, At), lva ).

	query ev: evPoison( At, cached_src_cname, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ).
	ERRORID8, ERRORID7, ERRORID6
*)

(* Properties in Section 7.2 *)
(* query ev: evPoison( At, makeSubName(bad, goddAuth), invalidIP, lv,
						cached_src_ns, makeSubName(good, goddAuth), cached_src_cname, eid ) ==>  
			ev: evInitCache( Record( makeSubName(good, goddAuth), validIP, At), lva ). 

   query ev: evPoison( At, makeSubName(bad, goddAuth), invalidIP, lv,
						cached_src_ns, makeSubName(good, goddAuth), cached_src_cname, eid ).
	ERRORID 0, 1, 9, 8, 7
*)

(* Properties in Section 7.3 *)
(* query ev: evPoison( At, cached_src_a, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ) 
	  ==> ev: evInitCache( Record( cached_src_a, cached_dst_a, At), lva ) & ga: lva, lv.  
  ( TRUE: in case, v6,v4 is true, FALSE: in case: v3{E7,E8-1,E9-1},v2{E7,E8,E9} ) 
*)

(* Properties in Section 7.4 *)
(* query ev: evPoison( NSt, cached_src_ns, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ) 
     ==> ev: evInitCache( Record( cached_src_ns, cached_dst_ns, NSt), lvns ) & ga: lvns, lv. 
	( FALSE in case any lvns lower than v6: v5{E4,E5-1},v3{E4,E5-1},v2{E4,E5} ) 
*)

 query ev: evPoison( CNAMEt, x, dst, lv, cached_src_ns, cached_src_a, cached_src_cname, eid ) 
	  ==>	ev: evInitCache( Record( target, validIP, At), lva ).


let processCC =	
	let v0 = zero in	let v1 = succ(v0) in
	let v2 = succ(v1) in	let v3 = succ(v2) in
	let v4 = succ(v3) in	let v5 = succ(v4) in
	let v6 = succ(v5) in	let v7 = succ(v6) in
	let v8 = succ(v7) in

	new currentState;
	new ansChannel;
	new authChannel;
	new addChannel;
						
	event StartResolver( currentState );

	(
	   (   
	(* Initialize a cache state. Based on this state, the resolver model makes a decision *)
	(* At first, the model cache two records: one of them is A type and another is NS type *)			
			new magicZONE;

			out( net, magicZONE );
			(* in ( net, ( initNSlabel, initClabel, initAlabel ) );  *)
			
			in ( net, ( makeSubName(NSlabel, =magicZONE), makeSubName(Clabel, =magicZONE), makeSubName(Alabel, =magicZONE) ) );

			let initNSlabel = makeSubName(NSlabel, magicZONE) in
			let initClabel  = makeSubName(Clabel, magicZONE) in
			let initAlabel  = makeSubName(Alabel, magicZONE) in
			
			let nsRoot = 
			Record( initNSlabel, ValidDN( dnmSeed ), NSt ) in (* Make a NS type record with a domain name and specified IP address *)
			let aRoot  = 
			Record( initAlabel, ValidIP( dnmIP ), At ) in  	(* Make a A type record with a domain name and specified IP address *)
			let cnameRoot = 
			Record( initClabel, ValidDN( cnmSeed ), CNAMEt ) in  (* In special case for modeling CNAME record in cache *)
  		  
			(* Assert an event declaring cached records with a certain trust levels *)
			event evInitCache( aRoot, v2 );     (* The trust level of CNAME can be or 6, 4, 3 or 2 *)
			event evInitCache( nsRoot, v2 );    (* The trust level of CNAME can be or 5, 3 or 2 *)
			event evInitCache( cnameRoot, v6 ); (* The trust level of CNAME can be or 6 or 4 *)
			
			(* currentState is a private internal channel, It is used for passing cached information to resolving process *)
         out( currentState, ( zeroStage, cnameRoot, aRoot, nsRoot, magicZONE ) )
	  )
	| (
			in( currentState, ( =zeroStage, cachedCNAMErecord, cachedArecord, cachedNSrecord, mZONE ) ); (* Get cache information from init process *)
	       !in( net, ( makeSubName(inputname, inputzone), inputtype) );  	 (* Get a query request from open channel network.*)
				
			let input = makeSubName(inputname, inputzone) in 

			event revQuery( input , inputtype );									 (* Assert an event that a query arrived *)

			(*If there is a cached CNAME type record whose label is same as a A type query then, resolution ends*)
			if ( input, inputtype, GetType(cachedCNAMErecord) ) = ( GetSrc( cachedCNAMErecord ), CNAMEt, CNAMEt ) then 
			(  event queryResolved( input, inputtype ) )
			else if ( input, inputtype, GetType(cachedCNAMErecord) ) = ( GetSrc( cachedCNAMErecord ), At, CNAMEt ) then 
			(	(* For CNAMEt, NS section and Additional sections are ignored by BIND resolver *)
				event queryResolved( input, inputtype )
			)
			else if ( input, inputtype ) = ( GetSrc( cachedNSrecord ), NSt ) then 
			(  event queryResolved( input, inputtype ) )
			(* If there is no record matching to a given query name and type, a recursive query starts. *)	
			else if ( input, inputtype ) <> ( GetSrc( cachedArecord ), GetType( cachedArecord ) ) then 
			(		
					let srcNSrecord = GetSrc( cachedNSrecord ) in 

					if input = srcNSrecord then
						out( currentState, ( oneStage, srcNSrecord, input, inputtype, cachedNSrecord, cachedArecord, cachedCNAMErecord ) )
					else if isSubName: input, srcNSrecord then
			         out( currentState, ( oneStage, srcNSrecord, input, inputtype, cachedNSrecord, cachedArecord, cachedCNAMErecord ) )
					else if input = mZONE then
						out( currentState, ( oneStage, mZONE, input, inputtype, cachedNSrecord, cachedArecord, cachedCNAMErecord ) )
					else if isSubName: input, mZONE then 
						out( currentState, ( oneStage, mZONE, input, inputtype, cachedNSrecord, cachedArecord, cachedCNAMErecord ) )
					else
						event resolvingFailed( input )
			) (* if ( input, inputtype ) <> ( GetSrc( cachedArecord ), GetType( cachedArecord ) )  *)
			else
			(  event queryResolved( input, inputtype ) )
		)
	|  ( 
			!in( currentState, (=oneStage, srcLabelCachedNS, input, inputtype, cachedNSrecord, cachedArecord, cachedCNAMErecord ) );	

			new dstLabelCachedNS;

			(* The query must be a subdomain name of zone determined by a resolver, otherwise it'll fail! *)
			if isSubName: input, srcLabelCachedNS then
			(				
				let bailiwickZone	= srcLabelCachedNS in

				(* Because, there is no data, the model start a recursive query. *)
				out( net, (input, inputtype) );					

				event recursiveQueryStart( input, srcLabelCachedNS, dstLabelCachedNS );
		
				(* And now waiting a response from a AA *)
				in( net, ( Response( =input, b, 
										   Record(auth_name, auth_target, =NSt), 
											Record(add_name, add_target, =At) ), aa ) );					

				let ans     = b in 
				let auth    = Record( auth_name, auth_target, NSt) in
				let add     = Record( add_name, add_target, At) in						    
		
				(		
					( 
						out( ansChannel, ( ansChID , input, inputtype, ans , aa, bailiwickZone, cachedNSrecord, cachedArecord, cachedCNAMErecord ) ) 
					)
				|  (
						if ans <> nil then out( authChannel, (authChID , input, inputtype, EXIST, auth, aa, bailiwickZone, cachedNSrecord, cachedArecord, cachedCNAMErecord) )
					)
				|  (
						if ans <> nil then out( addChannel,  (addChID  , input, inputtype, EXIST, auth, add, aa, bailiwickZone, cachedNSrecord, cachedArecord, cachedCNAMErecord) )
					)
				|  (
						if ans = nil then out( authChannel, (authChID , input, inputtype, NONEXIST , auth , aa, bailiwickZone, cachedNSrecord, cachedArecord, cachedCNAMErecord) )
					)
				|  (
						if ans = nil then out( addChannel,  (addChID  , input, inputtype, NONEXIST , auth , add, aa, bailiwickZone, cachedNSrecord, cachedArecord, cachedCNAMErecord) )
					)
				)

			)	(* if isSubName: input, srcLabelCachedNS then *)
		)
	|  ( 	
			(* Internal Answer Channel *)
	   	!in ( ansChannel, (=ansChID, inputR, inputtypeR, ansR, aaR, bailiwickZoneR, cachedNSrecordR, cachedArecordR, cachedCNAMErecordR ) );

			if GetType( ansR ) <> NSt then
		   (	
				if ansR <> nil then 
				(
					if ( inputR, inputtypeR ) = ( GetSrc( ansR ), GetType( ansR ) ) then 
					(
						if isSubName:  GetSrc(ansR), bailiwickZoneR then
						(
							if aaR = AAFLAG then
							(
									if checkrec: ansR then 	
										event evPoison( GetType(ansR), GetSrc(ansR), GetDst(ansR), v6,
												GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID0 )
							)
							else if checkrec: ansR then 	
								event evPoison( GetType(ansR), GetSrc(ansR), GetDst(ansR), v4, 
									GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID1 )
						)
					)
					else if ( inputR, inputtypeR, GetType( ansR ) ) = ( GetSrc( ansR ), At, CNAMEt ) then 
					(
						if isSubName:  GetSrc(ansR), bailiwickZoneR then
						(
							if aaR = AAFLAG then
							(
								if checkrec: ansR then 		
								(
									event evPoison( CNAMEt, GetSrc(ansR), GetDst(ansR), v6,
										GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID2 )
								)
							)
							else if checkrec: ansR then 	
								event evPoison( CNAMEt, GetSrc(ansR), GetDst(ansR), v4, 
										GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID3 )				
						)
					) (* else if ( inputR, inputtypeR, GetType( ansR ) ) = ( GetSrc( ansR ), At, CNAMEt ) then  *)
				 ) (* if ( inputR, inputtypeR ) = ( GetSrc( ansR ), GetType( ansR ) ) then  *)
			) (* if GetType( ansR ) <> NSt then *)
 		)
	|  ( 	
			(* Auth Channel *)
	    	!in ( authChannel, (=authChID, inputR, inputtypeR, ansR, authR, aaR, bailiwickZoneR, cachedNSrecordR, cachedArecordR, cachedCNAMErecordR ) );

    		if isSubName: GetSrc(authR), bailiwickZoneR then    
    		(	   
    			if (ansR,aaR) = (EXIST,AAFLAG) then
				(	
    				if checkrec: authR then (* trust_auth_AA *)
					  event evPoison( NSt, GetSrc(authR), GetDst(authR), v5, 
									GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID4 )   		
				) (* if (ansR,aaR) = (EXIST,AAFLAG) then *)
				else if GetSrc(authR) = bailiwickZoneR then    	
				(
					if checkrec: authR then (* trust_auth_AA *)
					(
						if aaR = AAFLAG then
						  event evPoison( NSt, GetSrc(authR), GetDst(authR), v5, 
										GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID5 )   		
						else
						  event evPoison( NSt, GetSrc(authR), GetDst(authR), v2, 
										GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID5 )   		
					)					
				)
				else if isSubName: inputR, GetSrc(authR) then 
				(			
					if checkrec: authR then (* trust_auth_AA *)
					(
						if aaR = AAFLAG then
						 	event evPoison( NSt, GetSrc(authR), GetDst(authR), v5, 
										GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID6 )   		
						else
							event evPoison( NSt, GetSrc(authR), GetDst(authR), v2, 
									GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID6 )
					)
				)
				else
				(
					event cachingAuthfail( authR )
				)
			) (* if isSubName: GetSrc(authR), bailiwickZoneR then *)
		)
	|  ( 	(* Add Channel *)
	    !in ( addChannel, (=addChID, inputR, inputtypeR, ansR, authR, addR, aaR, bailiwickZoneR, cachedNSrecordR, cachedArecordR, cachedCNAMErecordR ) );
    	    	   	
		if isSubName: GetSrc(authR), bailiwickZoneR then
	    	if isSubName: GetSrc(addR), bailiwickZoneR then
	    		if GetSrc(addR) = GetDst(authR) then    
    	(
    		event guideEvent3();
    			
    		if (ansR,aaR) = (EXIST,AAFLAG) then
			(	
    			if checkrec: addR then 
				   event evPoison( At, GetSrc(addR), GetDst(addR), v3, 
									GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID7 )   		
			)    					   
			
			(* else if isSubName: bailiwickZoneR, GetSrc(authR) then  *)
			else if GetSrc(authR) = bailiwickZoneR then    	
			(
				if checkrec: addR then 
				(
					if aaR = AAFLAG then
				   	event evPoison( At, GetSrc(addR), GetDst(addR), v3, 
									GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID8 )   		
					else
						event evPoison( At, GetSrc(addR), GetDst(addR), v2, 
									GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID8 )   		
				)				
			)		

	    	(* else if isSubName: GetSrc(addR), bailiwickZoneR then *)
			else if isSubName: inputR, GetSrc(authR) then 	
			(
				if inputR <> GetSrc(authR) then 
				(
					if checkrec: addR then 
					(
						if aaR = AAFLAG then
						  	event evPoison( At, GetSrc(addR), GetDst(addR), v3, 
									GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID9 ) 
						else
							event evPoison( At, GetSrc(addR), GetDst(addR), v2, 
									GetSrc(cachedNSrecordR), GetSrc(cachedArecordR), GetSrc(cachedCNAMErecordR), ERRORID9 ) 
					)
				)
				else event cachingGLUEfail( addR )
			)
			else
			(
				event cachingGLUEfail( addR )
			)
		)
	)
).		

process
	 processCC