KnoxV3.sapic

/*******************************************************************************
	Remote attestation Framework
	Protocol : Knox Attestation V2
	Status : Working

	* Processes
	AppCode : an honest app's logic 
	HonestAppInstallation : Allows installation of an honest app
	ArbitraryAppCode : An arbitrary app's logic
	ArbitraryAppInstallation : Allows installation of an arbitrary app
	Device : A mobile device process, it sets up a secure world and allows installing apps.
	AttestationAgent : A trusted attestation agent installed in a secure world to create a measurement report. 
	AtServer : An attestation server that verifies measurement reports.
	DevServer : The developer server of the honest apps. 
	RelayAttacker1 : An attacker process to retrieve a nonce from the developer server via a secure channel
	RelayAttacker2 : An attacker process to send the `hid` to the developer server via a secure channel

	* Channels
	SecureWorld_Ch_In : A secure channel from an app to a trusted agent to send app information
	SecureWorld_Ch_Out : A secure channel from a trusted agent to an app that sends the `hid`.
	Nonce_TLS_Ch : A secure channel from the developer server to send a nonce.
	HID_TLS_Ch: A secure channel from a client (an attacker or an app) to the developer server that sends the `hid`.
	HID_TLS_Ch_Out : A secure channel from the `AttestationAgent` to the attestation server that sends the `blob`.
	HID_TLS_Ch_In : A secure channel from the attestation server to the `AttestationAgent` that sends the `hid`.
	
	
*******************************************************************************/

theory Framework_KnoxV3
begin

builtins: signing, asymmetric-encryption, locations-report

heuristic: S

functions: 
	equal/2, and/2

predicates:
	Report(x,y) <=> not  (fst(y)= 'loc')
      
equations: 
	equal(x,x)=true,
	and(true,true)= true
	
/***************************************** Generic *****************************************/

let AppCode = 
	[Nonce_TLS_Ch(devId,nonce)]--[]-> [];

	event NonceReceivedAtApp(nonce);

	//attestation_agent send app data to secure world to start an attestation
	new ~sessionID;
	[]--[]-> [SecureWorld_Ch_In(~sessionID,~deviceId,swId,nonce,'App1PackageName','App1Content',sign(<'App1PackageName','App1Content',pk(advk)>,advk))];
	[ SecureWorld_Ch_Out(~sessionID,hid) ]--[]-> [];


	[]--[]-> [HID_TLS_Ch(hid)];
	event Checked('HonestAppFinished');
	0

let HonestAppInstallation =
	event Checked('HonestAppInstallation');
	//install an application
	[!App_Published(devId,<'App1PackageName','App1Content',pk(advk),
	                   sign( <'App1PackageName','App1Content',pk(advk)>, advk)>)]--[]-> [];

	event Application_Installed(~deviceId,'App1PackageName',sign(<'App1PackageName','App1Content',pk(advk)>, advk));

	!AppCode //App code separate from installation 


let ArbitraryAppCode =
	in(nonce);
	event NonceReceivedAtArbApp(nonce);
	//attestation_agent send app data to secure world to start an attestation
	new ~sessionID;
	[]--[]-> [SecureWorld_Ch_In(~sessionID,~deviceId,swId,nonce,packagename,~content,appSignature)];
	[ SecureWorld_Ch_Out(~sessionID,hid) ]--[]-> [];
	out(hid);
	event Checked('ArbitraryAppFinished');
	0

let ArbitraryAppInstallation =
	event Checked('ArbitraryAppInstallation');
	//install an application
	in(<packagename, devKey>); //Attacker can pick the app name and the dev key.

	new ~content;  //contents are different from any honest app, so we model as a free name
	let appSignature = sign(<packagename,~content,pk(devKey)>, devKey) in
	let app = <packagename,~content,pk(devKey),appSignature> in
	out(app);
	event Arbitrary_App_Created(packagename,appSignature);
	event Application_Installed(~deviceId,packagename,appSignature);

	!ArbitraryAppCode

let Device =

	//Create device reference
	new ~deviceId;   

	//send the device reference , allows an adversary to tamper the device
	out(~deviceId);
	
	//setup a secureWorld
	[]--[]-> [SetUPSW(~deviceId)];
	[FinishSetUPSW(~deviceId,swId)]--[]->[];
	event Checked('SettingUpDeviceFinished');

	(!HonestAppInstallation | !ArbitraryAppInstallation) 

let RelayAttacker1 = 
	[Nonce_TLS_Ch(devId,nonce)]--[]-> [];
	out(nonce);
	0

let RelayAttacker2 = 
	in(hid);
	[]--[]-> [HID_TLS_Ch(hid)];
	0
/***************************************** Knox V3 *****************************************/

let AtServerKV3 =
	!(

		//Retrive blob
		[HID_TLS_Ch_Out(tsid,<atId,nonce,hardwareMeasurement,packagename,appSignature,report,reportSignature>)]--[]-> [];

		//refernce blob to an hid
		new ~hid;
		//Send hid for the TZ
		[]--[]-> [HID_TLS_Ch_In(tsid,~hid)];

		//Retrive hid from the developer server and verfiy it
        [Attestation_Server_Ch_In(sid,~hid)]--[]-> [];

		//checking the blob location
		let locationCheck = equal(<atId,nonce,hardwareMeasurement,packagename,appSignature> , check_rep(report,<'loc',pk(~skAT)>)) in

		//checking the signature of the blob
		let signatureCheck = equal(verify(reportSignature, report,pk(~skAT)), true) in
		
		//check if both true
		let result = and(locationCheck, signatureCheck) in

		//create a verdict  and send it to the developer server
		if result = true then
			//create a verdict  and send it to the developer server
			let verdict = 'valid' in
			[]--[]-> [Attestation_Server_Ch_Out(sid,<verdict,atId,nonce,hardwareMeasurement,packagename,appSignature>)];
			event Checked('AttestationServerFinished_valid');
			0 
			
		else
			//create a verdict  and send it to the developer server
			let verdict = 'invalid' in
			[]--[]-> [Attestation_Server_Ch_Out(sid,<verdict,atId,nonce,hardwareMeasurement,packagename,appSignature>)];
			event Checked('AttestationServerFinished_invalid');
			0
	)


let KnoxV3TA =

	(
		new ~swId; // We have different secure world and device ID, because it's possible to make different devices have the same ID, therefore 

		//setup a SecureWorld
		[SetUPSW(deviceId)]--[]->[FinishSetUPSW(deviceId,~swId)];

		//attempt to unlock bootloader
		in(attempt);

		!(
			//attestation_agent send app data to secure world, start an attestation
			[SecureWorld_Ch_In(sessionID, deviceId,~swId,nonce,packagename,content,appSignature)]--[]->[];

			new ~tsid; //  attestation server hid session id
			new ~atId; // attestation id
			event Attestating_App(~atId,packagename,appSignature,deviceId);

			if attempt = 'unlockBootloader' then
				let hardwareMeasurement = 'invalid' in
				// Software measurment not used in Knox
				//in(customSoftwareMeasurement);
				//let softwareMeasurement =  customSoftwareMeasurement in
				in(<fnonce,fpackagename,fappSignature>);	// adversary's custom softeware-based values
				let report = report(<~atId,fnonce,hardwareMeasurement,fpackagename,fappSignature>) in 
				let blob = <~atId, fnonce, hardwareMeasurement,fpackagename,fappSignature, report,sign(report,~skAT)> in				///send attestation report to the attestation server
				[]--[]-> [HID_TLS_Ch_Out(~tsid,blob)];
				[HID_TLS_Ch_In(~tsid,hid)]--[]-> [];
				event BlobCreated(hid);
				out(hid);

				///return attestation report to the app
				event DeviceStatus(~atId,deviceId,hardwareMeasurement);
				event Attestating_App_Device(~atId,deviceId,packagename,appSignature,hardwareMeasurement);
				[]--[]->[ SecureWorld_Ch_Out(sessionID,hid) ];
				event Checked('SecureWorldAppFinished_rooted_device');
				0
			else
				let hardwareMeasurement = 'valid' in
				let report = report(<~atId,nonce,hardwareMeasurement,packagename,appSignature>) in 
				let blob = <~atId,nonce,hardwareMeasurement,packagename,appSignature,report,sign(report,~skAT)> in				///send attestation report to the attestation server
				[]--[]-> [HID_TLS_Ch_Out(~tsid,blob)];
				[HID_TLS_Ch_In(~tsid,hid)]--[]-> [];

				///return attestation report to the app
				event DeviceStatus(~atId,deviceId,hardwareMeasurement);
				event Attestating_App_Device(~atId,deviceId,packagename,appSignature,hardwareMeasurement);
				event BlobCreated(hid);
				[]--[]->[ SecureWorld_Ch_Out(sessionID,hid) ];
				event Checked('SecureWorldAppFinished_locked_device');
				0
				
		)
	)@<'loc',pk(~skAT)>

let DevServerProtocolCode =

	// create a nonce
	new ~nonce;
	event NonceGenerated(~nonce);
	new ~requestID;
    event BlobRequested(~requestID);
	[]--[]-> [Nonce_TLS_Ch(~devId,~nonce)];

	//retrive hid from clients
	[HID_TLS_Ch(hid)]--[]->[];


	//create developer-attestation server session id, to keep track or pair of request-response message  
	new ~sid;
	//send blob to the attestation server
	[]--[]-> [Attestation_Server_Ch_In(~sid,hid)];
	
	//retrieve the verfied report the attestation server, pattern matching is used for checking the status
	[Attestation_Server_Ch_Out(~sid,<verdict,atId,~nonce,hardwareMeasurement,fpackagename,fappSignature>)]--[]-> [];
	
	event NonceReceived(~nonce);

	//checking app information
	let appSignatureCheck = equal(appSignature, fappSignature) in
	let packagenameCheck = equal(packagename, fpackagename) in
	let result = and(appSignatureCheck, packagenameCheck) in
	
	//attestation finished		
	if result = true then
		event Verdict_app(atId,hid,verdict,hardwareMeasurement,'valid');
		event Checked('DeveloperServerfinished_valid');
		if verdict = 'valid' then
			event BlobAccepted(hid);
			event RequestedBlobAccepted(~requestID,hid)
		else 
			0
	else
		event Verdict_app(atId,hid,verdict,hardwareMeasurement,'invalid');
		event Checked('DeveloperServerfinished_invalid')
	


let DevServerKV3 =
	//creating and publishing the application
	new ~advk; // Dev server signing
	new ~devId; 

	let packagename = 'App1PackageName' in
	let appSignature = sign(<packagename,'App1Content',pk(~advk)>,~advk) in 
	let app = <packagename,'App1Content',pk(~advk),appSignature> in
	out(app);
	event App_Created(packagename,appSignature);

	[]--[]-> [!App_Published(~devId,app)];
	
	!DevServerProtocolCode

/*************************************** Generic code *************************************************/
	
// Main process starts here

/***************************************** choose a platform ***************************************************
* platform				|		SafetyNet			|		KnoxV2		|	KnoxV3			|	Key Attestation
* --------------------------------------------------------------------------------------------------------------
* AttestationAgent		: GooglePlay | SafetyNetTA	|	KnoxV2TA		|	KnoxV3TA		|	KeyMasterTA
* AtServer				:		AtServerSN			|	AtServerKV2		|	AtServerKV3		|	AtServerKA
* DevServer				:		DevServerSN			|	DevServerKV2	|	DevServerKV3	|	DevServerKA
***************************************************************************************************************/


let AttestationAgent =
	KnoxV3TA

let AtServer = 
	AtServerKV3

let DevServer = 
	DevServerKV3



//create pair attestation keys to be used by secureWorld for signing, and attestation server for verification
new ~skAT;

(!Device || !DevServer || AtServer || !AttestationAgent || !RelayAttacker1 || !RelayAttacker2)


//for all valid verdict => honest apps must created, installed, attested in a valid device and KU does know its attestation report
lemma DeviceAndAppIntegrity:
	"(All atId hid #i. Verdict_app(atId,hid,'valid','valid','valid') @ i ==> 
	( 
	 (Ex deviceId packagename appSignature #a #b #c. 
			 App_Created(packagename,appSignature) @ a
			 & Application_Installed(deviceId,packagename,appSignature) @ b
			 & Attestating_App_Device(atId,deviceId,packagename,appSignature,'valid')@ c 
			 & a < b & b < c & c < i
		)
	))"

//for all valid verdict =>  Ku should not know its attestation report by any mean
lemma AttestationReportSecrecy:
	"(All atId hid #i. Verdict_app(atId,hid,'valid','valid','valid') @ i ==> 
	 (	not( Ex #k. KU(hid) @ k & k<i ) )
	)"


// Check if nonce are unique 
// lemma UniqueNonce:
// "All n #i #j. NonceReceived(n) @i & NonceReceived(n) @j ==> #i=#j"

// Check if accepted blobs are unique 
lemma UniqueBlob:
"All n #i #j.  BlobAccepted(n) @i & BlobAccepted(n) @j ==> #i=#j"

// Check if the blob generated recently
lemma BlobRecentness:
    "All requestID blob #i. RequestedBlobAccepted(requestID,blob) @i ==> 
	  Ex #j. BlobRequested(requestID)@j & Ex #k. BlobCreated (blob)@k & #j < #k & #k < #i" 


//for all failed application integrity check only  => (device must be valid and there an app created, an app attested and either the hash is different or packagename).
lemma RepackedAppIntegrity:
"(All atId hid #i. Verdict_app(atId,hid,'valid','valid','invalid') @ i ==> 
( 
(Ex deviceId #j. DeviceStatus(atId,deviceId,'valid') @ j & j < i) 
& (Ex deviceId packagename fpackagename appSignature fappSignature #j #k. 
		 App_Created(packagename,appSignature) @ j 
		 & Attestating_App(atId,fpackagename,fappSignature,deviceId)@ k
		 & (
				(not(appSignature = fappSignature))
				| (not(packagename = fpackagename))
			 )
		 
	)
))"


//Sanity check: Will the dev server ever accept a blob
lemma Correctness_AcceptBlob:
exists-trace
"Ex n #i. BlobAccepted(n)@i"

//Sanity check: Attestation finished with valid device integirty and application integirty. 
lemma Correctness_Valid_Attestation:
exists-trace
"Ex atId blob #i. Verdict_app(atId,blob,'valid','valid','valid') @ i"

//Sanity check: Attestation finished with at least failed device integirty
lemma Correctness_Rooting_Device:
exists-trace
"Ex atId blob any #i. Verdict_app(atId,blob,'valid','invalid',any) @ i"

//Sanity check: Setting up a device's secure world 
lemma Correctness_Setting_Up_Device:
exists-trace
"Ex #i. Checked('SettingUpDeviceFinished') @ i"

//Sanity check: Creation of an honest application 
lemma Correctness_Honest_App:
exists-trace
"Ex #i. Checked('HonestAppInstallation') @ i"

//Sanity check: Creation of an arbitrary application 
lemma Correctness_Arbitrary_App:
exists-trace
"Ex #i. Checked('ArbitraryAppInstallation') @ i"

//Sanity check: An honest application can finish
lemma Correctness_Honest_App_Finished:
exists-trace
"Ex #i. Checked('HonestAppFinished') @ i"

//Sanity check: An arbitrary application can finish
lemma Correctness_Arbitrary_App_Finished:
exists-trace
"Ex #i. Checked('ArbitraryAppFinished') @ i"

//Sanity check: Secure world app can finish in a rooted device
lemma Correctness_Secure_World_Finished_ROOTED:
exists-trace
"Ex #i. Checked('SecureWorldAppFinished_rooted_device') @ i"

//Sanity check: Secure world app can finish in a locked device
lemma Correctness_Secure_World_Finished_LOCKED:
exists-trace
"Ex #i. Checked('SecureWorldAppFinished_locked_device') @ i"

//Sanity check: Attestation Server can finish with a verfied report 
lemma Correctness_Attestation_Server_Finished_VALID:
exists-trace
"Ex #i. Checked('AttestationServerFinished_valid') @ i"

//Sanity check: Attestation Server can finish with an invalid report 
lemma Correctness_Attestation_Server_Finished_INVALID:
exists-trace
"Ex #i. Checked('AttestationServerFinished_invalid') @ i"

//Sanity check: Developer server can finish with report from an honest app
lemma Correctness_Developer_Server_Finished_VALID:
exists-trace
"Ex #i. Checked('DeveloperServerfinished_valid') @ i"

//Sanity check: Developer server can finish with report from an arbitrary app
lemma Correctness_Developer_Server_Finished_INVALID:
exists-trace
"Ex #i. Checked('DeveloperServerfinished_invalid') @ i"

end

==============================================================================
summary of summaries:

analyzed: KnoxV3.sapic

	DeviceAndAppIntegrity (all-traces): verified (5 steps)
	AttestationReportSecrecy (all-traces): verified (5 steps)
	UniqueBlob (all-traces): verified (24 steps)
	BlobRecentness (all-traces): verified (14 steps)
	RepackedAppIntegrity (all-traces): verified (8 steps)
	Correctness_AcceptBlob (exists-trace): verified (3 steps)
	Correctness_Valid_Attestation (exists-trace): verified (4 steps)
	Correctness_Rooting_Device (exists-trace): verified (6 steps)
	Correctness_Setting_Up_Device (exists-trace): verified (4 steps)
	Correctness_Honest_App (exists-trace): verified (4 steps)
	Correctness_Arbitrary_App (exists-trace): verified (4 steps)
	Correctness_Honest_App_Finished (exists-trace): verified (4 steps)
	Correctness_Arbitrary_App_Finished (exists-trace): verified (4 steps)
	Correctness_Secure_World_Finished_ROOTED (exists-trace): verified (4 steps)
	Correctness_Secure_World_Finished_LOCKED (exists-trace): verified (4 steps)
	Correctness_Attestation_Server_Finished_VALID (exists-trace): verified (4 steps)
	Correctness_Attestation_Server_Finished_INVALID (exists-trace): falsified - no trace found (3 steps) //<<-- because the valid ones stored by the attestation server and the advasery cannot craft hid that has invalid measurement.
	Correctness_Developer_Server_Finished_VALID (exists-trace): verified (4 steps)
	Correctness_Developer_Server_Finished_INVALID (exists-trace): verified (6 steps)

==============================================================================