KeyAttestation_App_Code_Protection_Key.sapic

/*******************************************************************************
	Remote attestation Framework
	Protocol : Code protection (Secret key version) based on Android key attestation
	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 that creates a certificate chain `certificateChain`. 
	AtServer : An attestation server that published its root certificate.
	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 `certificateChain` 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 `certificateChain`.
	RequestCreatingIntermediateCertificate : A channel from the attesation server to the trusted agent `KeyMasterTA` to generate its certificate `intermediateCertificate`.
	
*******************************************************************************/

theory Framework_KeyAttestation_App_Nonce_CP_Key
begin

builtins: signing, asymmetric-encryption, locations-report

heuristic: S

predicates:
Report(x,y) <=> not  (fst(y)= 'loc')

functions: 
	create_certificate/3, verify_certificate/2 , get_tbsInfo_certificate/1, equal/2, and/2

equations:

    create_certificate(SubjectTBSCertificateInfo,SubjectPup,IssuerSk) 
      = < SubjectTBSCertificateInfo, SubjectPup, sign(<SubjectTBSCertificateInfo, SubjectPup>,IssuerSk) >,

    verify_certificate( 
    < SubjectTBSCertificateInfo, pk(SubjectSk), sign(<SubjectTBSCertificateInfo, pk(SubjectSk)>,IssuerSk) >
     , < IssuerTBSCertificateInfo, pk(IssuerSk), sign(<IssuerTBSCertificateInfo, pk(IssuerSk)>,IssuerRootSk) >
          ) = true,

    get_tbsInfo_certificate( 
        < SubjectTBSCertificateInfo, pk(SubjectSk), sign(<SubjectTBSCertificateInfo, pk(SubjectSk)>,IssuerSk) >
          ) = SubjectTBSCertificateInfo,
	
	equal(x,x)=true,
	and(true,true)= true
      


/***************************************** Generic *****************************************/

let AppCode = 

	in(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',cipherContent,secretVPk>,sign( <'App1PackageName',<'App1Content',cipherContent>,pk(advk)>,advk),pk(advk))];
	[ SecureWorld_Ch_Out(~sessionID,certificateChain) ]--[]-> [];
	out(certificateChain);

	in(cipher);
	
	[]--[]->[SecureWorld_Ch_In_2(~sessionID,cipher)];
	[SecureWorld_Ch_Out_2(~sessionID,<secretESk,signature>,hardwareMeasurement)]--[]->[];

	//check verfication for honest app. if the device already rooted. verfication can be bypassed
	if verify(signature,secretESk,secretVPk) = true  then
		event SecretOnlyReceivedAppStatus(~sessionID,secretESk,'valid');
		let content = adec(cipherContent,secretESk) in 
		event SecretReceivedAppStatus(~sessionID,content,secretESk,'valid');
		event Checked('HonestAppFinished');
		0	
	else if hardwareMeasurement = 'invalid' then
		event SecretOnlyReceivedAppStatus(~sessionID,secretESk,'valid');
		let content = adec(cipherContent,secretESk) in 
		event SecretReceivedAppStatus(~sessionID,content,secretESk,'valid');
		event Checked('HonestAppFinished');
		0		


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

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

	!AppCode 

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,pk(devKey))];
	[ SecureWorld_Ch_Out(~sessionID,certificateChain) ]--[]-> [];
	out(certificateChain);

	in(<cipher,cipherContent>);
	
	[]--[]->[SecureWorld_Ch_In_2(~sessionID,cipher)];
	[SecureWorld_Ch_Out_2(~sessionID,<secretESk,signature>,hardwareMeasurement)]--[]->[]; 
	//no need to check verfication here, because it is ArbitraryApp
	event SecretOnlyReceivedAppStatus(~sessionID,secretESk,'invalid');
	let content = adec(cipherContent,secretESk) in 
	event SecretReceivedAppStatus(~sessionID,content,secretESk,'invalid');
	event Checked('ArbitraryAppFinished');
	0


let ArbitraryAppInstallation =

	event Checked('ArbitraryAppInstallation');
	//install an application
	in(<packagename, devKey>); 

	new ~content;

	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)


/***************************************** Knox V3 *****************************************/

let AtServerKA =
	new ~rootSk;
	let rootCertificate = create_certificate('TbsInfo',pk(~rootSk),~rootSk) in

	//share root certficate	
	[]--[]->
	[
		!RequestCreatingIntermediateCertificate(~rootSk,rootCertificate),
		!GetRootCertificate(rootCertificate)
	];

	!(
		event Checked('AttestationServerFinished')
	)


let KeyMasterTA =

	(
	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)];

	
	//Request attestation server
	[!RequestCreatingIntermediateCertificate(rootSk,rootCertificate)]--[]->[];
	
	//Create keymaster certficate
	new ~keymasterSk;
	let  intermediateCertificate = create_certificate('TbsKeyStoreInfo',pk(~keymasterSk),rootSk) in

	//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,devPk)]--[]->[];

		new ~key;

		new ~atId;
		event Attestating_App(~atId,packagename,devPk,deviceId);

		if attempt = 'unlockBootloader' then
			let hardwareMeasurement = 'invalid' in
			//let softwareMeasurement = customSoftwareMeasurement in
			in(<fnonce,fpackagename,fdevPk>);	// adversary's custom softeware-based values
			let subjectCertificate = create_certificate(<~atId,hardwareMeasurement,nonce,packagename,fdevPk>,pk(~key),~keymasterSk) in
			let certificateChain = <subjectCertificate, intermediateCertificate, rootCertificate> in 
			//send attestation report to the app
			event DeviceStatus(~atId,deviceId,hardwareMeasurement);
			event Attestating_App_Device(~atId,deviceId,packagename,appSignature,hardwareMeasurement);
            event CreateCert(certificateChain);
			out(certificateChain);

			[]--[]->[ SecureWorld_Ch_Out(sessionID,certificateChain) ];

			[SecureWorld_Ch_In_2(sessionID, aenc(<secretESk,signature>,pk(~key)))]--[]->[];
			event SecretReceived(secretESk);
			event SecretReceivedatDevice(sessionID,secretESk,hardwareMeasurement);
			[]--[]->[SecureWorld_Ch_Out_2(sessionID,<secretESk,signature>,hardwareMeasurement)];

			event Checked('SecureWorldAppFinished_rooted_device');
			0
		else
			let hardwareMeasurement = 'valid' in
			//let softwareMeasurement = 'valid' in
			let subjectCertificate = create_certificate(<~atId,hardwareMeasurement,nonce,packagename,devPk>,pk(~key),~keymasterSk) in
			let certificateChain = <subjectCertificate, intermediateCertificate, rootCertificate> in 
			//send attestation report to the app
			event DeviceStatus(~atId,deviceId,hardwareMeasurement);
			event Attestating_App_Device(~atId,deviceId,packagename,appSignature,hardwareMeasurement);
            event CreateCert(certificateChain);
			[]--[]->[ SecureWorld_Ch_Out(sessionID,certificateChain) ];

			[SecureWorld_Ch_In_2(sessionID, aenc(<secretESk,signature>,pk(~key)))]--[]->[];
			event SecretReceived(secretESk);
			event SecretReceivedatDevice(sessionID,secretESk,hardwareMeasurement);
			[]--[]->[SecureWorld_Ch_Out_2(sessionID,<secretESk,signature>,hardwareMeasurement)];

			event Checked('SecureWorldAppFinished_locked_device');
			0
	
			
	)
	)@<'loc',pk(~skAT)>



let DevServerProtocolCode =
	
		// create a nonce
		new ~nonce;
		event NonceGenerated(~nonce);
        new ~requestID;
        event RequestCert(~requestID);
		out(~nonce);
		
		//retrieve blob from clients
		in(<<<atId,hardwareMeasurement,~nonce,fpackagename,fdevPk>,subjectPk,subjectChain>, intermediateCertificate, rootCertificate>);
		let certificateChain = <<<atId,hardwareMeasurement,~nonce,fpackagename,fdevPk>,subjectPk,subjectChain>, intermediateCertificate, rootCertificate> in
		let subjectTbs = <atId,hardwareMeasurement,~nonce,fpackagename,fdevPk> in
		let subjectCertificate = <subjectTbs,subjectPk,subjectChain> in
		[!GetRootCertificate(rootCertificate)]--[]->[];
		
		event NonceReceived(~nonce);

		//verify certificate chain
		let verfication = and(
			verify_certificate(subjectCertificate, intermediateCertificate),
			verify_certificate(intermediateCertificate, rootCertificate)
		) in

		//checking app information
		let appCertificateCheck = equal(pk(~advk) , fdevPk) in
		let packagenameCheck = equal(packagename, fpackagename) in
		let result = and(appCertificateCheck, packagenameCheck) in

		//encrypt the secret encryption key
		let signature = sign(~secretESk,~secretVSk) in 
		let cipher = aenc(<~secretESk,signature>, subjectPk) in
		
		if verfication = true then
			if result = true  then
				event AcceptCert(~requestID,<subjectCertificate, intermediateCertificate, rootCertificate>);
				event Verdict_app(atId,certificateChain,'valid',hardwareMeasurement,'valid');
				event Checked('DeveloperServerfinished_valid');
				if hardwareMeasurement = 'valid' then
					event BlobAccepted(certificateChain);
					out(cipher)
				else
					0
			else
				event Verdict_app(atId,certificateChain,'valid',hardwareMeasurement,'invalid');
				event Checked('DeveloperServerfinished_invalid')



let DevServerKA =

	//generate secret
	new ~secretContent;
	event SecretContentGenerated(~secretContent);
	
	//secret verfication key
	new ~secretVSk;
	out(pk(~secretVSk));

	//secret encryption key
	new ~secretESk;
	out(pk(~secretESk));
	event SecretEKeyGenerated(~secretESk);

	event SecretGenerated(~secretContent,~secretESk);

	//generate cipher
	let cipherContent = aenc(<~secretContent>,pk(~secretESk)) in

	//creating and publishing the application
	new ~advk; // Dev server signing key
	new ~devId; 
	let packagename = 'App1PackageName' in
	let content = <'App1Content',cipherContent,pk(~secretVSk)> in
	let appSignature = sign( <'App1PackageName',content,pk(~advk)>,~advk) in 
	let app = <'App1PackageName',content,pk(~advk),appSignature> in
	out(app);
	event App_Created(packagename,pk(~advk));

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


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

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


let AttestationAgent =
	KeyMasterTA

let AtServer = 
	AtServerKA

let DevServer = 
	DevServerKA




//create pair attetsation keys to be used by secreworld for sigining, and attestation server for verfication
new ~skAT;

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


lemma CertPossible:
  exists-trace 
    "Ex requestID subjectCertificate intermediateCertificate rootCertificate #i #j.
        (AcceptCert(requestID,<subjectCertificate, intermediateCertificate, rootCertificate>) @i
        & RequestCert(requestID)@j) & #j < #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"

lemma BlobRecentness:
"All requestID blob #i.
	AcceptCert(requestID,blob) @i
		==>   Ex #j. RequestCert(requestID)@j
			& Ex #k. CreateCert (blob)@k
			& #j < #k & #k < #i" 


lemma CorrectnessValidSecret:
	exists-trace
		"Ex secretContent secretESk  sessionID #i #j #k. SecretGenerated(secretContent,secretESk) @i & SecretReceivedatDevice(sessionID,secretESk,'valid')@j & SecretReceivedAppStatus(sessionID,secretContent,secretESk,'valid')@k & (#i<#j) & (#j<#k)"
	
lemma SecretValidity:
	all-traces
		"All secretContent secretESk  sessionID #j #k. SecretReceivedatDevice(sessionID,secretESk,'valid')@j & SecretReceivedAppStatus(sessionID,secretContent,secretESk,'valid')@k ==>
		(Ex #i. SecretGenerated(secretContent,secretESk) @i & (#i<#j) & (#j<#k))"
	

lemma SecretSecrecy:
	all-traces
		"All secretContent secretESk  #i. SecretGenerated(secretContent,secretESk) @i ==> 
		(not(Ex #k. KU(<secretContent,secretESk>)@k & (#i<#k)))
		& (not(Ex sessionID #k. SecretReceivedAppStatus(sessionID,secretContent,secretESk,'invalid')@k  & (#i<#k) ))
		& (not(Ex sessionID #j. SecretReceivedatDevice(sessionID,secretESk,'invalid')@j & (#i<#j)))"
	
//Desc: Doliv-yao should not be able to know secrets generated by an honest developer
//For all secrets, generated by an honest developer, then there is no exist an advsery know at least one of these secrets.
lemma SecretSecrecyKU:
	all-traces
		"All secretContent secretESk #i. SecretGenerated(secretContent,secretESk) @i ==> (not(Ex #k. KU(<secretContent,secretESk>)@k & (#i<#k)))"

//Desc: Repacked app should not be able to know secrets generated by an honest developer
//For all secrets, generated by an honest developer, and receved by a valid device => then, there is no exist a secret recvied by an arbitrary app.
lemma SecretSecrecyAgainstRepakedApp:
	all-traces
		"All secretContent secretESk #i . SecretGenerated(secretContent,secretESk) @i  ==>
			(not(Ex sessionID #k. SecretReceivedAppStatus(sessionID,secretContent,secretESk,'invalid')@k  & (#i<#k) ))"

//Desc: Rooted device should not be able to know secrets generated by an honest developer
//For all traces, it is not possibile for a secret generated by an honest developer to be retrieved/known/leaked by a rooted device.
lemma SecretSecrecyAgainstRootedDevice:
	all-traces
		"All secretContent secretESk  #i. SecretGenerated(secretContent,secretESk) @i ==> (not(Ex sessionID #j. SecretReceivedatDevice(sessionID,secretESk,'invalid')@j & (#i<#j)))"

//Desc: KU advseray should not be able to inject key into an honest app that run on an honest device 
//For all secrets that recieved by a valid device and loaded by an honest app to be known by adversary
lemma KeyInjection:
	all-traces
		"All  secretESk sessionID #i #k.SecretReceivedatDevice(sessionID,secretESk,'valid')@i &  KU(secretESk) @k  ==>
			(not(Ex #j. SecretOnlyReceivedAppStatus(sessionID,secretESk,'valid')@j & (#i<#j)))"

//can rooted device, inecjt valid app? yes becuase the device rooted. full control over everything
// Code injection on rooted device : It is a possibile for a remote advsery to inject a key intro an honest app  if the device under the attacker control.
lemma KeyInjectionByRootedDevice:
exists-trace
		"(Ex  secretESk sessionID #i #j #k. SecretReceivedatDevice(sessionID,secretESk,'invalid')@i & SecretOnlyReceivedAppStatus(sessionID,secretESk,'valid')@j & KU(secretESk)@k  & (#i<#j))"


//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
lemma Correctness_Attestation_Server_Finished:
exists-trace
	"Ex #i. Checked('AttestationServerFinished') @ 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: KeyAttestation_App_Code_Protection_Key.sapic

	CertPossible (exists-trace): verified (13 steps)
	UniqueBlob (all-traces): verified (8 steps)
	BlobRecentness (all-traces): verified (76 steps)
	CorrectnessValidSecret (exists-trace): verified (17 steps)
	SecretValidity (all-traces): verified (17 steps)
	SecretSecrecy (all-traces): verified (165 steps)
	SecretSecrecyKU (all-traces): verified (21 steps)
	SecretSecrecyAgainstRepakedApp (all-traces): verified (73 steps)
	SecretSecrecyAgainstRootedDevice (all-traces): verified (72 steps)
	KeyInjection (all-traces): verified (86 steps)
	KeyInjectionByRootedDevice (exists-trace): verified (9 steps)
	Correctness_Valid_Attestation (exists-trace): verified (13 steps)
	Correctness_Rooting_Device (exists-trace): verified (13 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 (8 steps)
	Correctness_Arbitrary_App_Finished (exists-trace): verified (7 steps)
	Correctness_Secure_World_Finished_ROOTED (exists-trace): verified (6 steps)
	Correctness_Secure_World_Finished_LOCKED (exists-trace): verified (6 steps)
	Correctness_Attestation_Server_Finished (exists-trace): verified (4 steps)
	Correctness_Developer_Server_Finished_VALID (exists-trace): verified (13 steps)
	Correctness_Developer_Server_Finished_INVALID (exists-trace): verified (13 steps)

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