/******************************************************************************* Modelling and Analysis of 802.11 4-Way Handshake Attacks and Security Properties AUTHORS Attack against the 4-way handshake, when the supplicant when (victim) still accepts plaintext retransmissions of message 3 if 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_fig4_msr 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 // =================== // Initialization MSRs // =================== // // Single authenticator allowed, multiple supplicants allowed rule Authenticator_Init: [ Fr(~pmk), Fr(~A_id) ] --[ Init() ]-> [ !SharedKey(~pmk), !Authenticator_Initiated(~pmk, ~A_id), Out(~A_id) ] rule Supplicant_Init: [ !SharedKey(~pmk), Fr(~S_id) ] --[ ]-> [ !Supplicant_Initiated(~pmk, ~S_id), Out(~S_id) ] // =============== // Supplicant Setup MSRs // =============== rule Supplicant_out_AuthRequest: [ !Supplicant_Initiated(~pmk, ~S_id) ] --[ ]-> [ Supplicant_Sent_AuthRequest(~pmk, ~S_id), Out(<'AuthRequest', ~S_id>) ] rule Supplicant_in_AuthResponse_out_AuthRequest: [ Supplicant_Sent_AuthRequest(~pmk, ~S_id), In(<'AuthResponse', ~S_id, cs>) ] --[ ]-> [ Supplicant_Sent_AssociationRequest(~pmk, ~S_id, cs), Out(<'AssociationRequest', ~S_id, cs>) ] rule Supplicant_in_AssociationResponse_in_Aid: [ Supplicant_Sent_AssociationRequest(~pmk, ~S_id, cs), In(<'AssociationResponse', ~S_id, cs>), Fr(~tid), In(A_id) ] --[ S_HasPmk(~S_id, ~pmk) ]-> [ Supplicant_Received_AssociationResponse(~pmk, ~S_id, cs, A_id, ~tid) ] // ================== // Authenticator Setup MSRs // ================== rule Authenticator_in_AuthRequest_out_AuthResponse: [ !Authenticator_Initiated(~pmk, ~A_id), Fr(~tid), In(<'AuthRequest', S_id>) ] --[ ]-> [ Authenticator_Sent_AuthResponse(~pmk, ~A_id, S_id, ~tid), Out(<'AuthResponse', S_id, 'CCMP'>) ] rule Authenticator_in_AssociationRequest_out_AssociationResponse: let cs = 'CCMP' in [ Authenticator_Sent_AuthResponse(~pmk, ~A_id, S_id, ~tid), In(<'AssociationRequest', S_id, cs>), In(S_id) ] --[ A_HasPmk(~A_id, ~pmk) ]-> [ Authenticator_Sent_AssociationResponse(~pmk, ~A_id, S_id, ~tid, cs), Out(<'AssociationResponse', S_id, cs>) ] // Supplicant 4WHS // Authenticator 4WHS rule A1: let msg1_contents = <'Header1', ~r, ~ANonce, cs> in [ Authenticator_Sent_AssociationResponse(~pmk, ~A_id, S_id, ~tid, cs), In(S_id), Fr(~r), Fr(~ANonce) ] --[ LogA1(~A_id, S_id,~ANonce) ]-> [ Authenticator_Sent_Msg1(~pmk, ~A_id, S_id, ~tid, cs, ~r, ~ANonce), Out(msg1_contents) ] rule S2: let msg1_contents = <'Header1', r, ANonce, cs> msg2_contents = <'Header2', r, ~SNonce, cs> tptk = CalcPtk(<~pmk, ANonce, ~SNonce, A_id, ~S_id>) in [ Supplicant_Received_AssociationResponse(~pmk, ~S_id, cs, A_id, ~tid), In(msg1_contents), Fr(~SNonce) ] --[ S_ComputesPtk(~S_id, ~tid, tptk), LogS2(A_id, ~S_id, ANonce, ~SNonce) ]-> [ Supplicant_Sent_Msg2(~pmk, ~S_id, cs, A_id, ~tid, ANonce, ~SNonce, r, tptk), Out()>) ] rule A3: let ptk = CalcPtk(<~pmk, ~ANonce, SNonce, ~A_id, S_id>) msg2_contents = <'Header2', ~r, SNonce, cs> msg3_contents = <'Header3', ~r+'1', ~ANonce, cs, senc(~gtk, )> in [ Authenticator_Sent_Msg1(~pmk, ~A_id, S_id, ~tid, cs, ~r, ~ANonce), In()>), Fr(~gtk) ] --[ LogA3(~A_id, S_id,~ANonce,SNonce,ptk,~gtk), A_GeneratesGtk(~gtk), A_RunningPtk(~A_id, S_id, ptk), A_RunningGtk(~A_id, S_id, <~ANonce, SNonce, ~gtk>), A_RunningCs(~A_id, S_id, <~ANonce, SNonce, cs>), A_InstallsGtk(~gtk) // MLME-SETKEYS.request ]-> [ Authenticator_Sent_Msg3(~pmk, ~A_id, S_id, ~tid, cs, ~r, ~ANonce, SNonce, ptk, ~gtk), Out()>) ] rule S4: let msg3_contents = <'Header3', r+'1', ANonce, cs, senc(gtk, )> msg4_contents = <'Header4', r+'1', cs> ptk = tptk in [ Supplicant_Sent_Msg2(~pmk, ~S_id, cs, A_id, ~tid, ANonce, ~SNonce, r, tptk), In()>) ] --[ LogS4(A_id, ~S_id,ANonce, ~SNonce,ptk,gtk), S_ReceivesGtk(~S_id, ~tid, gtk), S_RunningPtk(~S_id, A_id, ptk), S_RunningGtk(~S_id, A_id, ), S_RunningCs(~S_id, A_id, ), S_InstallsPtk(~S_id, ptk), // MLME-SETKEYS.request S_InstallsGtk(~S_id, gtk) // MLME-SETKEYS.request ]-> [ Supplicant_Sent_Msg4(~pmk, ~S_id, cs, A_id, ~tid, ANonce, ~SNonce, r, tptk, gtk), Out()>) ] rule S5: // Normal finish let ptk = tptk in [ Supplicant_Sent_Msg4(~pmk, ~S_id, cs, A_id, ~tid, ANonce, ~SNonce, r, tptk, gtk) ] --[ LogS5(A_id, ~S_id, ANonce, ~SNonce,ptk,gtk), S_CommitPtk(~S_id, A_id, ptk), S_CommitGtk(~S_id, A_id, ), S_CommitCs(~S_id, A_id, ), S_Branch1() ]-> [ ] rule A6: // Msg3 retransmission let msg3_rtx_contents = <'Header3', ~r+'1'+'1', ~ANonce, cs, senc(~gtk, )> in [ Authenticator_Sent_Msg3(~pmk, ~A_id, S_id, ~tid, cs, ~r, ~ANonce, SNonce, ptk, ~gtk) ] --[ LogA6(~A_id, S_id, ~ANonce, SNonce,ptk,~gtk)]-> [ Authenticator_Sent_Msg3rtx(~pmk, ~A_id, S_id, ~tid, cs, ~r, ~ANonce, SNonce, ptk, ~gtk), Out()>) ] rule S7: // Retransmission let msg3_rtx_contents = <'Header3', r+'1'+'1', ANonce, cs, senc(gtk2, )> msg4_rtx_contents = <'Header4', r+'1'+'1', cs> ptk = tptk in [ Supplicant_Sent_Msg4(~pmk, ~S_id, cs, A_id, ~tid, ANonce, ~SNonce, r, tptk, gtk), In()>) ] --[ LogS7(A_id, ~S_id, ANonce, ~SNonce,ptk,gtk), S_RunningPtk(~S_id, A_id, ptk), S_RunningGtk(~S_id, A_id, ), S_RunningCs(~S_id, A_id, ), S_InstallsPtk(~S_id, ptk), // MLME-SETKEYS.request S_InstallsGtk(~S_id, gtk) // MLME-SETKEYS.request ]-> [ Supplicant_Sent_Msg4rtx(~pmk, ~S_id, cs, A_id, ~tid, ANonce, ~SNonce, r, tptk, gtk), Out(senc()>, tk(ptk))) ] rule S8: // Finish after retransmission let ptk = tptk in [ Supplicant_Sent_Msg4rtx(~pmk, ~S_id, cs, A_id, ~tid, ANonce, ~SNonce, r, tptk, gtk) ] --[ LogS8(A_id, ~S_id, ANonce, ~SNonce,ptk,gtk), S_CommitPtk(~S_id, A_id, ptk), S_CommitGtk(~S_id, A_id, ), S_CommitCs(~S_id, A_id, ), S_Branch2() ]-> [ ] rule A9: // Finish after retransmission let msg4_rtx_contents = <'Header4', ~r+'1'+'1', cs> in [ Authenticator_Sent_Msg3rtx(~pmk, ~A_id, S_id, ~tid, cs, ~r, ~ANonce, SNonce, ptk, ~gtk), In(senc()>, tk(ptk))) ] --[ LogA9(~A_id, S_id, ~ANonce, SNonce,ptk,~gtk), A_InstallsPtk(ptk), // MLME-SETKEYS.request A_CommitPtk(~A_id, S_id, ptk), A_CommitGtk(~A_id, S_id, <~ANonce, SNonce, ~gtk>), A_CommitCs(~A_id, S_id, <~ANonce, SNonce, cs>), A_Branch2() ]-> [ ] rule A10: // Normal finish let msg4_contents = <'Header4', ~r+'1', cs> in [ Authenticator_Sent_Msg3(~pmk, ~A_id, S_id, ~tid, cs, ~r, ~ANonce, SNonce, ptk, ~gtk), In()>) ] --[ LogA10(~A_id,S_id, ~ANonce, SNonce,ptk,~gtk), A_InstallsPtk(ptk), // MLME-SETKEYS.request A_CommitPtk(~A_id, S_id, ptk), A_CommitGtk(~A_id, S_id, <~ANonce, SNonce, ~gtk>), A_CommitCs(~A_id, S_id, <~ANonce, SNonce, cs>), A_Branch1() ]-> [ ] /* lemma Debug: exists-trace "Ex #i. Debug()@i" */ restriction single_session: "All #i #j. ((Init()@ #i) & (Init()@ #j)) ==> (#i = #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 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 (pmk1=pmk2)" // b) Ensure that the security association keys are fresh. lemma FreshPtk: all-traces "All id tid1 tid2 ptk #t1 #t2. S_ComputesPtk(id, tid1, ptk)@t1 & S_ComputesPtk(id, tid2, ptk)@t2 ==> (tid1=tid2)" lemma FreshGtk: all-traces "All id tid1 tid2 gtk #t1 #t2. S_ReceivesGtk(id, tid1, gtk)@t1 & S_ReceivesGtk(id, tid2, gtk)@t2 ==> (tid1=tid2)" // c) Synchronize the installation of one or more temporal keys into the MAC. lemma AgreementPtk: all-traces "(All X Y ptk #i. A_CommitPtk(X, Y, ptk)@i ==> ((Ex #j. S_RunningPtk(Y, X, ptk)@j & (j ((Ex #j. A_RunningPtk(Y, X, ptk)@j & (j ((Ex #j. S_RunningGtk(Y, X, gtk)@j & (j ((Ex #j. A_RunningGtk(Y, X, gtk)@j & (j (not (Ex #j. K(ptk)@j))" lemma SecretGtk: all-traces "All id gtk #i. S_InstallsGtk(id, gtk)@i ==> (not (Ex #j. K(gtk)@j))" // d) Transfer the GTK from the Authenticator to the Supplicant. lemma SameGtk: all-traces "All S gtk #i. S_InstallsGtk(S, gtk)@i ==> (Ex #j. A_GeneratesGtk(gtk)@j & (j ((Ex #j. S_RunningCs(Y, X, cs)@j & (j ((Ex #j. A_RunningCs(Y, X, cs)@j & (j (#i=#j)" lemma NoGtkReuse: all-traces "All id gtk #i #j. S_InstallsGtk(id, gtk)@i & S_InstallsGtk(id, gtk)@j ==> (#i=#j)" // Uncomment the following to enforce restrictions and verify the proposed as well as standard properties // Enforcing f) as restrictions /* restriction RestNoPtkReuse: "All id ptk #i #j. S_InstallsPtk(id, ptk)@i & S_InstallsPtk(id, ptk)@j ==> (#i=#j)" restriction RestNoGtkReuse: "All id gtk #i #j. S_InstallsGtk(id, gtk)@i & S_InstallsGtk(id, gtk)@j ==> (#i=#j)" */ end /* MSR WITHOUT RESTRICTIONS ============================================================================== summary of summaries: analyzed: k4.spthy CorrectnessS1 (exists-trace): verified (11 steps) CorrectnessS2 (exists-trace): verified (13 steps) CorrectnessA1 (exists-trace): verified (12 steps) CorrectnessA2 (exists-trace): verified (14 steps) NoKrackPtk (all-traces): falsified - found trace (16 steps) ConfirmPmk (all-traces): verified (4 steps) FreshPtk (all-traces): verified (2 steps) FreshGtk (all-traces): verified (31 steps) AgreementPtk (all-traces): verified (90 steps) AgreementGtk (all-traces): verified (123 steps) SecretPtk (all-traces): verified (8 steps) SecretGtk (all-traces): verified (36 steps) SameGtk (all-traces): verified (32 steps) AgreementCs (all-traces): verified (90 steps) NoPtkReuse (all-traces): falsified - found trace (17 steps) NoGtkReuse (all-traces): falsified - found trace (18 steps) ============================================================================== real 0m42.887s user 1m31.975s sys 0m13.269s */ /* MSR WITH RESTRICTIONS ============================================================================== summary of summaries: analyzed: k4.spthy CorrectnessS1 (exists-trace): verified (11 steps) CorrectnessS2 (exists-trace): falsified - no trace found (2 steps) CorrectnessA1 (exists-trace): verified (12 steps) CorrectnessA2 (exists-trace): verified (14 steps) NoKrackPtk (all-traces): verified (2 steps) ConfirmPmk (all-traces): verified (4 steps) FreshPtk (all-traces): verified (2 steps) FreshGtk (all-traces): verified (2 steps) AgreementPtk (all-traces): verified (75 steps) AgreementGtk (all-traces): verified (93 steps) SecretPtk (all-traces): verified (6 steps) SecretGtk (all-traces): verified (12 steps) SameGtk (all-traces): verified (10 steps) AgreementCs (all-traces): verified (76 steps) NoPtkReuse (all-traces): verified (2 steps) NoGtkReuse (all-traces): verified (2 steps) ============================================================================== real 0m6.811s user 0m17.017s sys 0m1.999s */