KeyAttestation_App_NoNonce.sapic

/*******************************************************************************
	Remote attestation Framework
	Protocol : 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`.
	Certificate_TLS_Ch: A secure channel from a client (an attacker or an app) to the developer server 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_NoNonce
begin

builtins: signing, asymmetric-encryption, locations-report

heuristic: S

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

predicates:
	Report(x,y) <=> not  (fst(y)= 'loc')
      
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 = 

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

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

let ArbitraryAppCode =
	in(requestID);
	//attestation_agent send app data to secure world to start an attestation
	new ~sessionID;
	[]--[]-> [SecureWorld_Ch_In(~sessionID,~deviceId,swId,packagename,~content,appSignature,pk(devKey))];
	[ SecureWorld_Ch_Out(~sessionID,certificateChain) ]--[]-> [];
	event ArbitraryBlob(certificateChain);
	out(certificateChain);
	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)


let RelayAttacker = 
	in(certificateChain);
	[]--[]-> [Certificate_TLS_Ch(certificateChain)];
	0

/***************************************** 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 the bootloader
	in(attempt);

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

		//create subject certificate's key
		new ~key;

		new ~atId;
		event Attestating_App(~atId,packagename,devPk,deviceId);
		
		//get current timestamp
		in(cdate);

		if attempt = 'unlockBootloader' then
			let hardwareMeasurement = 'invalid' in
			//let softwareMeasurement = customSoftwareMeasurement in
			in(<fpackagename,fdevPk>);	// adversary's custom softeware-based values
			let subjectCertificate = create_certificate(<~atId,hardwareMeasurement,cdate,fpackagename,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);
			event BlobCreated(certificateChain);
			out(certificateChain);

			[]--[]->[ SecureWorld_Ch_Out(sessionID,certificateChain) ];
			event Checked('SecureWorldAppFinished_rooted_device');
			0
		else
			let hardwareMeasurement = 'valid' in
			//let softwareMeasurement = 'valid' in
			let subjectCertificate = create_certificate(<~atId,hardwareMeasurement,cdate,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);
			event BlobCreated(certificateChain);
			[]--[]->[ SecureWorld_Ch_Out(sessionID,certificateChain) ];
			event Checked('SecureWorldAppFinished_locked_device');
			0			
	)
	)@<'loc',pk(~skAT)>


let DevServerProtocolCode =

		new ~requestID;
        event BlobRequested(~requestID);
				
		//retrieve certificate chain from clients
		[Certificate_TLS_Ch(<<<atId,hardwareMeasurement,cdate,fpackagename,fdevPk>,subjectPk,subjectChain>, intermediateCertificate, rootCertificate>)]--[]-> [];
		let certificateChain = <<<atId,hardwareMeasurement,cdate,fpackagename,fdevPk>,subjectPk,subjectChain>, intermediateCertificate, rootCertificate> in
		let subjectTbs = <atId,hardwareMeasurement,cdate,fpackagename,fdevPk> in
		let subjectCertificate = <subjectTbs,subjectPk,subjectChain> in
		[!GetRootCertificate(rootCertificate)]--[]->[];
		
		//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

		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');
				event RequestedBlobAccepted(~requestID,certificateChain);
				if hardwareMeasurement = 'valid' then
					event BlobAccepted(certificateChain)
				else 
					0
			else
				event Verdict_app(atId,certificateChain,'valid',hardwareMeasurement,'invalid');
				event Checked('DeveloperServerfinished_invalid')
		else
			0


let DevServerKA =
	//creating and publishing the application
	new ~advk; // Dev server signing key
	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 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 || !RelayAttacker)


lemma CertPossible:
  exists-trace 
    "Ex requestID blob #i #j.
        (RequestedBlobAccepted(requestID,blob) @i
        & BlobRequested(requestID)@j) & #j < #i "

//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 certificateChain #i. Verdict_app(atId,certificateChain,'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 certificateChain #i. Verdict_app(atId,certificateChain,'valid','valid','valid') @ i ==> 
	 (	not( Ex #k. KU(certificateChain) @ k & k<i ) )
	)"

/// 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 certificateChain #i. Verdict_app(atId,certificateChain,'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"

//lemma Correctness_AcceptArbitraryBlob:
//exists-trace
//"Ex n #i #j. BlobAccepted(n)@i & ArbitraryBlob(n)@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_NoNonce.sapic

  CertPossible (exists-trace): verified (4 steps)
  DeviceAndAppIntegrity (all-traces): verified (16 steps)
  AttestationReportSecrecy (all-traces): verified (16 steps)
  UniqueBlob (all-traces): verified (38 steps)
  BlobRecentness (all-traces): falsified (4 steps)
  RepackedAppIntegrity (all-traces): verified (52 steps)
  Correctness_AcceptBlob (exists-trace): verified (4 steps)
  Correctness_Valid_Attestation (exists-trace): verified (4 steps)
  Correctness_Rooting_Device (exists-trace): verified (5 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 (exists-trace): verified (4 steps)
  Correctness_Developer_Server_Finished_VALID (exists-trace): verified (4 steps)
  Correctness_Developer_Server_Finished_INVALID (exists-trace): verified (5 steps)

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