/*******************************************************************************
	TITLE
	AUTHORS
	
	Attack against the 4-way handshake, when the supplicant only accepts
	encrypted message 3 retransmissions once a PTK is installed.
	
	Notation:
	
	pmk = Pairwise Master Key
	ptk = Pairwise Transient Key, composed of:
		kck = Key Confirmation Key
		kek = Key Encryption Key
		tk = Temporal Key
	gtk = Group Temporal Key
	
	A_  = Events only in authenticator process
	S_  = Events only in supplicant process
	
*******************************************************************************/

theory Krack_fig6_003
begin

builtins:
	symmetric-encryption,
	multiset

functions:
	true/0,
	CalcPTK/1,
	mic/2,
	kck/1,
	kek/1,
	tk/1,
	verifyMic/3

equations: 
	verifyMic(mic(m,k), m, k) = true



let Supplicant =
	new ~S_id;
	out(~S_id);

	!(
		// Initial 4-way handshake
		new ~tid;
		
		in(A_id);
		
		let pat_msg1_contents = <'Header1', r, ANonce> in
		in(pat_msg1_contents);
		event Receive(A_id, ~S_id, 'Message1', r, pat_msg1_contents);
		
		new ~SNonce;
		let tptk = CalcPTK(<~pmk, ANonce, ~SNonce, A_id, ~S_id>) in
		event S_ComputesPTK(~tid, tptk);
		
		let msg2_contents = <'Header2', r, ~SNonce> in
		event Send(~S_id, A_id, 'Message2', r, msg2_contents);
		out(<msg2_contents, mic(msg2_contents, kck(tptk))>);
		
		let msg3_contents = <'Header3', r+'1', ANonce, senc(gtk, kek(tptk))> in
		in(<msg3_contents, mic(msg3_contents, kck(tptk))>);
		event Receive(A_id, ~S_id, 'Message3', r+'1', msg3_contents);
		
		let ptk = tptk in
		
		event Running(~S_id, A_id, <~SNonce, ANonce, r+'1', ptk, gtk>);
		
		let msg4_contents = <'Header4', r+'1'> in
		event Send(~S_id, A_id, 'Message4', r+'1', msg4_contents);
		out(<msg4_contents, mic(msg4_contents, kck(ptk))>);

		event S_InstallsPtk(~S_id, ptk); // MLME-SETKEYS.request
		event S_InstallsGtk(~S_id, gtk); // MLME-SETKEYS.request
		
		event Commit(~S_id, A_id, <ANonce, ~SNonce, r, ptk, gtk>);
		
		// Pairwise rekey
		!(
			new ~tid2;
		
			let rekey_msg1_contents = <'Header1', r2, ANonce2> in
			let m = rekey_msg1_contents in
			in(senc(m, tk(ptk)));
			event Receive(A_id, ~S_id, 'Message1', r2, rekey_msg1_contents);
			event DcpReceive(~S_id, m, tk(ptk));			

			event S_ReplayCtr(r2);
			event S_AcceptsMessage(~S_id, m);			

			new ~SNonce2;
			let tptk2 = CalcPTK(<~pmk, ANonce2, ~SNonce2, A_id, ~S_id>) in
			event S_ComputesPTK(~tid2, tptk2);
			
			let rekey_msg2_contents = <'Header2', r2, ~SNonce2> in
			let m = <rekey_msg2_contents, mic(rekey_msg2_contents, kck(tptk2))> in
			event Send(~S_id, A_id, 'Message2', r2, rekey_msg2_contents);
			event DcpSend(~S_id, m, tk(ptk));			
			out(senc(m, tk(ptk)));

			let rekey_msg3_contents = <'Header3', r2+'1', ANonce2, senc(gtk2, kek(tptk2))> in
			let m = <rekey_msg3_contents, mic(rekey_msg3_contents, kck(tptk2))> in
			in(senc(m, tk(ptk)));
			event Receive(A_id, ~S_id, 'Message3', r2+'1', rekey_msg3_contents);
			event DcpReceive(~S_id, m, tk(ptk));	

			event S_ReplayCtr(r2+'1');
			event S_AcceptsMessage(~S_id, m);
			
			let ptk2 = tptk2 in
					  
			event Running(~S_id, A_id, <~SNonce2, ANonce2, r2+'1', ptk2, gtk2>);
			
			((
				let rekey_msg4_contents = <'Header4', r2+'1'> in
																	 
				let m = <rekey_msg4_contents, mic(rekey_msg4_contents, kck(ptk2))> in
				event Send(~S_id, A_id, 'Message4', r2+'1', rekey_msg4_contents);
				event DcpSend(~S_id, m, tk(ptk));			
				out(senc(m, tk(ptk)));
				
				event S_InstallsPtk(~S_id, ptk2); // MLME-SETKEYS.request
				event S_InstallsGtk(~S_id, gtk2); // MLME-SETKEYS.request
				
				event Commit(~S_id, A_id, <ANonce2, ~SNonce2, r2, ptk2, gtk2>);				
				event S_Branch1()
			) +
			(
				let rekey_msg3_rtx_contents = <'Header3', r2+'1'+'1', ANonce2, senc(gtk2, kek(tptk2))> in
				let m = <rekey_msg3_rtx_contents, mic(rekey_msg3_rtx_contents, kck(tptk2))> in
				in(senc(m, tk(ptk)));
				event Receive(A_id, ~S_id, 'Message3', r2+'1'+'1', rekey_msg3_rtx_contents);
				event DcpReceive(~S_id, m, tk(ptk));
				
				event S_ReplayCtr(r2+'1'+'1');
				event S_AcceptsMessage(~S_id, m);

				let ptk2 = tptk2 in
				
				event Running(~S_id, A_id, <~SNonce2, ANonce2, r2+'1'+'1', ptk2, gtk2>);
				
				let rekey_msg4_contents = <'Header4', r2+'1'> in
				let m = <rekey_msg4_contents, mic(rekey_msg4_contents, kck(ptk2))> in
				event Send(~S_id, A_id, 'Message4', r2+'1', rekey_msg4_contents);
				event DcpSend(~S_id, m, tk(ptk));			
				out(senc(m, tk(ptk)));
				
				event S_InstallsPtk(~S_id, ptk2); // MLME-SETKEYS.request
				event S_InstallsGtk(~S_id, gtk2); // MLME-SETKEYS.request				

				let rekey_msg4_rtx_contents = <'Header4', r2+'1'+'1'> in
				let m = <rekey_msg4_rtx_contents, mic(rekey_msg4_rtx_contents, kck(ptk2))> in
				event Send(~S_id, A_id, 'Message4', r2+'1'+'1', rekey_msg4_rtx_contents);
				event DcpSend(~S_id, m, tk(ptk));			
				out(senc(m, tk(ptk)));
				
				event S_InstallsPtk(~S_id, ptk2); // MLME-SETKEYS.request
				event S_InstallsGtk(~S_id, gtk2); // MLME-SETKEYS.request				
		
				event Commit(~S_id, A_id, <ANonce2, ~SNonce2, r2, ptk2, gtk2>);				
				event S_Branch2()
			))
		)
	)

	
	

let Authenticator =
	new ~A_id;
	out(~A_id);
	
	!(
		// Initial 4-way handshake
		
		new ~r;
		new ~ANonce;
		
		in(S_id);
		
		let pat_msg1_contents = <'Header1', ~r, ~ANonce> in
		event Send(~A_id, S_id, 'Message1', ~r, pat_msg1_contents);
		out(pat_msg1_contents);

		let ptk = CalcPTK(<~pmk, ~ANonce, SNonce, ~A_id, S_id>) in
		let msg2_contents = <'Header2', ~r, SNonce> in
		in(<msg2_contents, mic(msg2_contents, kck(ptk))>);
		event Receive(S_id, ~A_id, 'Message2', ~r, msg2_contents);
		
		new ~gtk;
		event A_GeneratesGtk(~gtk);
		event Running(~A_id, S_id, <~ANonce, SNonce, ~r, ptk, ~gtk>);
		event A_InstallsGtk(~gtk); // MLME-SETKEYS.request
		
		let msg3_contents = <'Header3', ~r+'1', ~ANonce, senc(~gtk, kek(ptk))> in
		event Send(~A_id, S_id, 'Message3', ~r+'1', msg3_contents);
		out(<msg3_contents, mic(msg3_contents, kck(ptk))>);
		
		let msg4_contents = <'Header4', ~r+'1'> in
		in(<msg4_contents, mic(msg4_contents, kck(ptk))>);
		event Receive(S_id, ~A_id, 'Message4', ~r+'1', msg4_contents);		
			
		event A_InstallsPtk(ptk); // MLME-SETKEYS.request
		
		event Commit(~A_id, S_id, <SNonce, ~ANonce, ~r+'1', ptk, ~gtk>);

		// Pairwise rekey
		!(
			new ~r2; //TODO it's new??
			new ~ANonce2;
			
			let rekey_msg1_contents = <'Header1', ~r2, ~ANonce2> in
			let m = rekey_msg1_contents in
			event Send(~A_id, S_id, 'Message1', ~r2, rekey_msg1_contents);
			event DcpSend(~A_id, m, tk(ptk));			
			out(senc(m, tk(ptk)));
	
			let ptk2 = CalcPTK(<~pmk, ~ANonce2, SNonce2, ~A_id, S_id>) in
			let rekey_msg2_contents = <'Header2', ~r2, SNonce2> in
			let m = <rekey_msg2_contents, mic(rekey_msg2_contents, kck(ptk2))> in
			in(senc(m, tk(ptk)));
			event Receive(S_id, ~A_id, 'Message2', ~r2, rekey_msg2_contents);
			event DcpReceive(~A_id, m, tk(ptk));			

			//let gtk2 = ~gtk in  // No gtk rekeying
			new ~gtk2;
			event A_GeneratesGtk(~gtk2);
			event Running(~A_id, S_id, <~ANonce2, SNonce2, ~r2, ptk2, ~gtk2>);
			event A_InstallsGtk(~gtk2); // MLME-SETKEYS.request
			
			let rekey_msg3_contents = <'Header3', ~r2+'1', ~ANonce2, senc(~gtk2, kek(ptk2))> in
			let m = <rekey_msg3_contents, mic(rekey_msg3_contents, kck(ptk2))> in
			event Send(~A_id, S_id, 'Message3', ~r2+'1', rekey_msg3_contents);
			event DcpSend(~A_id, m, tk(ptk));			
			out(senc(m, tk(ptk)));
						
			((
				let rekey_msg4_contents = <'Header4', ~r2+'1'> in
				let m = <rekey_msg4_contents, mic(rekey_msg4_contents, kck(ptk2))> in
				in(senc(m, tk(ptk)));
				event Receive(S_id, ~A_id, 'Message4', ~r2+'1', rekey_msg4_contents);
				event DcpReceive(~A_id, m, tk(ptk));	
			
				event A_InstallsPtk(ptk2); // MLME-SETKEYS.request

				event Commit(~A_id, S_id, <SNonce2, ~ANonce2, ~r2+'1', ptk2, ~gtk2>);
				event A_Branch1()
			) +
			(
				let rekey_msg3_rtx_contents = <'Header3', ~r2+'1'+'1', ~ANonce2, senc(~gtk2, kek(ptk2))> in
				let m = <rekey_msg3_rtx_contents, mic(rekey_msg3_rtx_contents, kck(ptk2))> in
				event Send(~A_id, S_id, 'Message3', ~r2+'1'+'1', rekey_msg3_rtx_contents);
				event DcpSend(~A_id, m, tk(ptk));			
				out(senc(m, tk(ptk)));
				
				let rekey_msg4_rtx_contents = <'Header4', ~r2+'1'+'1'> in
				let m = <rekey_msg4_rtx_contents, mic(rekey_msg4_rtx_contents, kck(ptk2))> in
				in(senc(m, tk(ptk)));
				event Receive(S_id, ~A_id, 'Message4', ~r2+'1'+'1', rekey_msg4_rtx_contents);
				event DcpReceive(~A_id, m, tk(ptk));	

				event A_InstallsPtk(ptk2); // MLME-SETKEYS.request

				event Commit(~A_id, S_id, <SNonce2, ~ANonce2, ~r2+'1'+'1', ptk2, ~gtk2>);
				event A_Branch2()
			))
		)
	)


// Main process starts here
new ~pmk; (!Supplicant || Authenticator)


// Uncomment to apply countermeasure.
//restriction CountermeasureKrackPtk:
//	"All id ptk #i #j. S_InstallsPtk(id, ptk)@i & S_InstallsPtk(id, ptk)@j ==> (#i=#j)"

restriction RestrictionCtr:
	"All r r2 #i #j. S_ReplayCtr(r)@i & S_ReplayCtr(r2)@j & (i<j) ==> (Ex x. r+x=r2)"

lemma DataConfProtocolInvariant [sources]:
	"All id1 m k #i. DcpReceive(id1, m, k)@i ==> 
		( (Ex #j. KU(m)@j & (j<i))
		| (Ex id2 #j. DcpSend(id2, m, k)@j) 
		)"

lemma CorrectnessS1:
exists-trace
	"Ex #i. S_Branch1()@i"

// This lemma is expected to be falisified after activating countermeasure.
lemma CorrectnessS2:
exists-trace
	"Ex #i. S_Branch2()@i"		
	
lemma CorrectnessA1:
exists-trace
	"Ex #i. A_Branch1()@i"

lemma CorrectnessA2:
exists-trace
	"Ex #i. A_Branch2()@i"

// The supplicant will not accept replayed messages
lemma CorrectnessNoReplay:
	"All id m #i #j. S_AcceptsMessage(id, m)@i & S_AcceptsMessage(id, m)@j ==> (#i=#j)"

// The KRACK attack does not exist.
lemma NoKrackPtk:
	"All id ptk #i. S_InstallsPtk(id, ptk)@i ==> not(Ex #j. S_InstallsPtk(id, ptk)@j & (j<i))"

// PTK is secret - It is not possible that the PTK has been installed and the adversary knows it.
lemma SecretPtk:
all-traces
	"All id ptk #i. S_InstallsPtk(id, ptk)@i  ==> (not (Ex #j. K(ptk)@j))"

// GTK is secret - It is not possible that the GTK has been installed and the adversary knows it.
lemma SecretGtk:
all-traces
	"All id gtk #i. S_InstallsGtk(id, gtk)@i  ==> (not (Ex #j. K(gtk)@j))"

// GTK accepted by one of the supplicants is the GTK calculated and forwarded by the authenticator.
lemma ReceivedGtkSameAsGenerated:
all-traces
	"All S gtk #i. S_InstallsGtk(S, gtk)@i  ==> (Ex #j. A_GeneratesGtk(gtk)@j & (j<i))" 

// PTK is fresh.
lemma FreshPtk: 
all-traces
	"All tid1 tid2 ptk #i #j. S_ComputesPTK(tid1, ptk)@i & S_ComputesPTK(tid2, ptk)@j ==> (tid1=tid2)"

// Agreement [Lowe97]
//  - Injective (assumed from definition)
//  - Full, t = <X.Nonce, Y.Nonce, ptk, gtk> 
//  - Mutual
lemma Agreement:
all-traces
	"All X Y t #i. Commit(X, Y, t)@i ==>
		( (Ex #j. Running(Y, X, t)@j & (j<i))
		& not(Ex X2 Y2 #i2. Commit(X2, Y2, t)@i2 & not(#i2=#i))
		)"

/*
lemma MessageOrdering:
all-traces
	"(All X Y MessageN r m #i #j.
		Send(X, Y, MessageN, r, m)@i & Receive(X, Y, MessageN, r, m)@j ==> (i<j))
	&(All X Y r m #i1. 
		Send(X, Y, 'Message2', r, m)@i1 ==> (Ex m1 #j1. Receive(Y, X, 'Message1', r, m1)@j1 & (j1<i1)))
	&(All X Y r m #i2.
		Send(X, Y, 'Message3', r, m)@i2 ==> (Ex r1 m1 #j2. Receive(Y, X, 'Message2', r1, m1)@j2 & (j2<i2)))
	&(All X Y r m #i3.
		Send(X, Y, 'Message4', r, m)@i3 ==> (Ex m1 #j3. Receive(Y, X, 'Message3', r, m1)@j3 & (j3<i3)))
	"
*/

end


// WITHOUT COUNTERMEASURE
// ==============================================================================
// summary of summaries:
//
// analyzed: krack_fig6_003.sapic
//
  // DataConfProtocolInvariant (all-traces): verified (1505 steps)
  // CorrectnessS1 (exists-trace): verified (15 steps)
  // CorrectnessS2 (exists-trace): verified (16 steps)
  // CorrectnessA1 (exists-trace): verified (16 steps)
  // CorrectnessA2 (exists-trace): verified (17 steps)
  // CorrectnessNoReplay (all-traces): verified (40 steps)
  // NoKrackPtk (all-traces): falsified - found trace (19 steps)
  // SecretPtk (all-traces): verified (233 steps)
  // SecretGtk (all-traces): verified (1616 steps)
  // ReceivedGtkSameAsGenerated (all-traces): verified (580 steps)
  // FreshPtk (all-traces): verified (12 steps)
  // Agreement (all-traces): verified (3092 steps)
//
// ==============================================================================
// real    45m57.844s
// user    105m35.473s
// sys     17m17.926s



// WITH COUNTERMEASURE
// ==============================================================================
// summary of summaries:
//
// analyzed: krack_fig6_003.sapic
//
  // DataConfProtocolInvariant (all-traces): verified (1505 steps)
  // CorrectnessS1 (exists-trace): verified (15 steps)
  // CorrectnessS2 (exists-trace): falsified - no trace found (2 steps)
  // CorrectnessA1 (exists-trace): verified (16 steps)
  // CorrectnessA2 (exists-trace): verified (17 steps)
  // CorrectnessNoReplay (all-traces): verified (40 steps)
  // NoKrackPtk (all-traces): verified (2 steps)
  // SecretPtk (all-traces): verified (162 steps)
  // SecretGtk (all-traces): verified (1134 steps)
  // ReceivedGtkSameAsGenerated (all-traces): verified (400 steps)
  // FreshPtk (all-traces): verified (12 steps)
  // Agreement (all-traces): verified (2702 steps)
//
// ==============================================================================
// real    33m59.629s
// user    78m36.576s
// sys     12m47.085s