From 83b04fc8e471d692fdf43171e669c32fde9fd7cc Mon Sep 17 00:00:00 2001 From: Kevin Milner Date: Thu, 4 May 2017 23:08:55 +0100 Subject: PSK mode readded --- wireguard.m4 | 122 +++++++++++++++++++++++++++++++++++------------------------ 1 file changed, 72 insertions(+), 50 deletions(-) diff --git a/wireguard.m4 b/wireguard.m4 index 9123eff..dfe23ee 100644 --- a/wireguard.m4 +++ b/wireguard.m4 @@ -66,6 +66,9 @@ rule PSKKeyGen: --[PSKey(~psk)]-> [ !AgentPSK(~psk) ] +rule NoPSKMode: + []--[PSKey('nopsk')]->[!AgentPSK('nopsk')] + /* Key Reveals for our adversary model */ rule PSK_reveal: [ !AgentPSK(k) ] --[ Reveal_PSK(k) ]-> [ Out(k) ] @@ -83,6 +86,7 @@ rule AddPublicKey: let pkB = 'g'^~ltkB in [ !AgentKey(~ltkA) , !AgentKey(~ltkB) + , !AgentPSK('nopsk') , Fr(~id) ]--[]-> [ // For search efficiency, state is divided into @@ -90,10 +94,17 @@ rule AddPublicKey: // allows tamarin to immediately bind the keys back // to this initial pairing rule. The fresh ~id is used // to identify this pairing. - State(~id, 'nopsk', 'nostate') + State(~id,'nopsk','NoMessageState') , !StateInvariants(~id, ~ltkA, pkB, pkB^~ltkA) ] +rule ChangePSK: + [ State(~id,oldpsk,anything) + , !AgentPSK(psk) + ]--[]-> + [ State(~id,psk,'NoMessageState') + ] + // MESSAGE RULES rule Handshake_Init: let pkI = 'g'^~ltkI @@ -115,19 +126,21 @@ rule Handshake_Init: [ //Init can be triggered at any time, even when currently performing //another role or on another stage. This could happen e.g. because of a timeout. //As such we bind the previous state as 'anything' and discard it. - State(~id,'nopsk',anything) + State(~id,psk,anything) , !StateInvariants(~id, ~ltkI, pkR, sisr) , Fr(~sidI) , Fr(~ekI) // The pkISurrogate is used later to approximate identity hiding. , Fr(~pkISurrogate) - ]--[]-> + ]--[ + UsingPSK(psk) + ]-> [ //We cache DH sisr to reduce variant precomputation time for tamarin. - State(~id,'nopsk',<'init',~sidI,~ekI,ci2,ki2,hi1>) + State(~id,psk,<'init',~sidI,~ekI,ci2,ki2,hi1>) , !EphKeytoReveal(~ekI) //This is a heuristic hack, so that the heuristic can prioritize solving for //the init rule without prioritizing the State() fact. - , F_SolveInit(~id,'nopsk',<'init',~sidI,~ekI,ci2,ki2,hi1>) + , F_SolveInit(~id,psk,<'init',~sidI,~ekI,ci2,ki2,hi1>) , Out(m1) ] @@ -155,26 +168,27 @@ rule Handshake_Resp: hr2 = h() cr4 = h() cr5 = h() - cr6 = h() //TODO: replace 'nopsk' with actual psk, maybe revealed maybe not - hrt = h() - kr6 = h() + cr6 = h() //TODO: replace 'nopsk' with actual psk, maybe revealed maybe not + hrt = h() + kr6 = h() hr3 = h() aempt = aead(kr6,'e',hr3) hr4 = h() m2 = <'2',sidI,~sidR,pekR,aempt,$mac1,$mac2> in - [ State(~id,'nopsk',anything) + [ State(~id,psk,anything) , !StateInvariants(~id,~ltkR,pkI,sisr) , Fr(~ekR) , Fr(~sidR) , In(m1) ]--[ - RKeys() //Not actually cr6, but derived from it. + RKeys() //Not actually cr6, but derived from it. , Identity_Surrogate(pkISurrogate) + , UsingPSK(psk) ]-> - [ State(~id,'nopsk',<'transport_unconfirmed',~sidR,pekI,pekR,cr6>) + [ State(~id,psk,<'transport_unconfirmed',~sidR,pekI,pekR,cr6>) //This is a heuristic hack, so that the heuristic can prioritize solving for //the resp rule without prioritizing the State() fact. - , F_SolveResp(~id,'nopsk',<'transport_unconfirmed',~sidR,pekI,pekR,cr6>) + , F_SolveResp(~id,psk,<'transport_unconfirmed',~sidR,pekI,pekR,cr6>) , !EphKeytoReveal(~ekR) , Out(m2) ] @@ -189,9 +203,9 @@ rule Handshake_Complete: hi2 = h() ci4 = h() ci5 = h() - ci6 = h() //TODO: see note above about using real psk instead of 'nopsk' - hit = h() - ki6 = h() + ci6 = h() //TODO: see note above about using real psk instead of 'nopsk' + hit = h() + ki6 = h() hi3 = h() aempt = aead(ki6,'e',hi3) hi4 = h() @@ -199,14 +213,15 @@ rule Handshake_Complete: //We assume the first transport message is 'as weak as possible', that is all values //in it are public except the key used to encrypt. mtr = <'4',sidR,aead(ci6,'message','0')> in - [ State(~id,'nopsk',<'init',sidI,~ekI,ci2,ki2,hi1>) - , F_SolveInit(~id,'nopsk',<'init',sidI,~ekI,ci2,ki2,hi1>) + [ State(~id,psk,<'init',sidI,~ekI,ci2,ki2,hi1>) + , F_SolveInit(~id,psk,<'init',sidI,~ekI,ci2,ki2,hi1>) , !StateInvariants(~id,~ltkI,pkR,sisr) , In(m2) ]--[ - IKeys() //Not actually ci6, but derived from it. + IKeys() //Not actually ci6, but derived from it. + , UsingPSK(psk) ]-> - [ State(~id,'nopsk',<'transport',sidI,ci3>) + [ State(~id,psk,<'transport',sidI,ci3>) , Out(mtr) ] @@ -274,26 +289,6 @@ lemma R_disagreement_implies_Si_or_SrEr_compromise[reuse]: //Or both R's static and ephemeral were already compromised | (Ex #j #j2. Reveal_AK(pkr) @ j & Reveal_EphK(pekr) @ j2 & #j2 < #i & #j < #i)" -lemma disagreement_implies_noPSK_or_compromisedPSK[reuse]: - "(All pki pkr peki pekr psk ck #i. - //If I believes they have completed a handshake with R - IKeys() @ i - //but R does not have a matching session - & not(Ex #j. #j < #i & RKeys() @ j) - ==> //Then either they aren't in PSK mode - (psk = 'nopsk') - //Or the adversary compromised the PSK before the session - | (Ex #j. #j < #i & Reveal_PSK(psk) @ j)) - &(All pki pkr peki pekr psk ck #i. - //If R believes they have a confirmed session with I - RConfirm() @ i - //but I does not have a matching session - & not(Ex #j. #j < #i & IKeys() @ j) - ==> //Then either they aren't in PSK mode - (psk = 'nopsk') - //Or the adversary compromised the PSK before the session - | (Ex #j. #j < #i & Reveal_PSK(psk) @ j))" - lemma session_uniqueness: //For both I and R, a 'confirmed session key' will always be unique (even if all keys are compromised) //This follows from I and R generating random ephemeral values. Note that this could be violated if the @@ -309,17 +304,6 @@ lemma session_uniqueness: // All autoprove, but key_secrecy takes forever ///////////////////////////////////////////////////////////////////////////// -lemma secrecy_without_psk_compromise: - "(All pki pkr peki pekr psk ck #i #j. - //If the adversary ever knows a session key that I derived from a handshake - IKeys() @ i & K(ck) @ j - ==> //Then either the adversary revealed the PSK, or there was no PSK - (Ex #j2. Reveal_PSK(psk) @ j2) | (psk = 'nopsk')) - //& similarly for R - &(All pki pkr peki pekr psk ck #i #j. - RConfirm() @ i & K(ck) @ j - ==> (Ex #j2. Reveal_PSK(psk) @ j2) | (psk = 'nopsk'))" - lemma key_secrecy[reuse]: "(All pki pkr peki pekr psk ck #i #i2. //If I and R agree on keys @@ -342,5 +326,43 @@ lemma identity_hiding: ==> //Then the adversary compromised at least one of R's static, I's static, or I's ephemeral (Ex #j. Reveal_AK(pkr) @ j) | (Ex #j. Reveal_AK(pki) @ j) | (Ex #j. Reveal_EphK(peki) @ j)" +//////// PSK PROPERTIES ///////////////////////////////////////////////////// +// These require a helper lemma that slows down the things above. +///////////////////////////////////////////////////////////////////////////// + +lemma psk_invariant_helper[reuse,use_induction]: + "All psk #i. UsingPSK(psk) @ i ==> Ex #j. #j < #i & PSKey(psk) @ j" + +lemma disagreement_implies_noPSK_or_compromisedPSK[reuse]: + "(All pki pkr peki pekr psk ck #i. + //If I believes they have completed a handshake with R + IKeys() @ i + //but R does not have a matching session + & not(Ex #j. #j < #i & RKeys() @ j) + ==> //Then either they aren't in PSK mode + (psk = 'nopsk') + //Or the adversary compromised the PSK before the session + | (Ex #j. #j < #i & Reveal_PSK(psk) @ j)) + &(All pki pkr peki pekr psk ck #i. + //If R believes they have a confirmed session with I + RConfirm() @ i + //but I does not have a matching session + & not(Ex #j. #j < #i & IKeys() @ j) + ==> //Then either they aren't in PSK mode + (psk = 'nopsk') + //Or the adversary compromised the PSK before the session + | (Ex #j. #j < #i & Reveal_PSK(psk) @ j))" + +lemma secrecy_without_psk_compromise: + "(All pki pkr peki pekr psk ck #i #j. + //If the adversary ever knows a session key that I derived from a handshake + IKeys() @ i & K(ck) @ j + ==> //Then either the adversary revealed the PSK, or there was no PSK + (Ex #j2. Reveal_PSK(psk) @ j2) | (psk = 'nopsk')) + //& similarly for R + &(All pki pkr peki pekr psk ck #i #j. + RConfirm() @ i & K(ck) @ j + ==> (Ex #j2. Reveal_PSK(psk) @ j2) | (psk = 'nopsk'))" + end // vim: ft=spthy -- cgit v1.2.3-59-g8ed1b