diff options
Diffstat (limited to 'wireguard.m4')
-rw-r--r-- | wireguard.m4 | 61 |
1 files changed, 40 insertions, 21 deletions
diff --git a/wireguard.m4 b/wireguard.m4 index e48b7f3..83046a2 100644 --- a/wireguard.m4 +++ b/wireguard.m4 @@ -9,7 +9,7 @@ changecom(<!@,@!>) * Status: Basically complete? Use the 'i' heuristic to autoprove. * * TODO: - * - Implement identity hiding properly using observational equivalence. + * - Implement identity hiding using observational equivalence, instead of the weaker surrogate-based property. * - Prove indistinguishability using observational equivalence. * - Model ECDH(private, NULL) = NULL */ @@ -18,15 +18,23 @@ theory WireGuard begin builtins: hashing, diffie-hellman -/* We're not going to model the nonce in the aead, since it's always 0 in the handshake. */ +/* Normally an aead would be arity 4, but in the handshake the nonce is always + * the fixed value 0 so for legibility we do not include it */ functions: aead/3, decrypt/2, verify/3, true/0 /* The plaintext can be recovered with the key */ equations: decrypt(aead(k, p, a), k) = p /* The authentication can be checked with the key and AAD */ equations: verify(aead(k, p, a), a, k) = true +/* This restriction tells Tamarin that whenever an Eq( ) fact occurs, + * the terms in it must be equal. This allows us to model rules that + * only trigger if e.g. the AEAD correctly verifies */ restriction Eq_testing: "All x y #i. Eq(x, y) @ i ==> x = y" +/* === m4 Definitions === + * These are mostly used to influence Tamarin's heuristics. They can be + * commented out by prefixing them with 'dnl'. */ + /* Uncomment these to prevent any adversary message modifications, * useful for checking exists-trace lemmas and making sure messsages * don't require the adversary to reorder terms etc. */ @@ -44,7 +52,9 @@ define(StateInvariants, F_StateInvariants($*)) * case, typically agent state can come from just about anywhere so it creates * a ton of case distinctions when we're usually only interested in the current * session anyway. */ -define(State, L_State($*)) /* HACK: This is a heuristic hack that should be removed by prefixing with m4 comment - d n l. */ +define(State, L_State($*)) + +/* === Setup and key reveal rules === */ /* Keygen is separate from pairing to allow keys to be paired * more than once (if they were generated fresh in the pairing @@ -55,7 +65,7 @@ rule AgentKeyGen: [!AgentKey(~ltk), Out('g'^~ltk)] /* Semi-malicious or ignorant agents might share a PSK with multiple - * parties, so we'll overapproximate this by allowing it to be shared + * parties, so we overapproximate this by allowing the same PSK to be reused * arbitrarily. If this finds an attack then it may not be a 'real' * attack, but if it doesn't then there is no problem with PSK reuse. */ rule PSKKeyGen: @@ -63,7 +73,9 @@ rule PSKKeyGen: --[PSKey(~psk)]-> [ !AgentPSK(~psk) ] -/* Key Reveals for our adversary model */ +/* Key Reveals for our adversary model. These allow the adversary to reveal + * any of the keys below at any time, unless restricted in the lemma we wish + * to prove. */ rule PSK_reveal: [ !AgentPSK(k) ] --[ Reveal_PSK(k) ]-> [ Out(k) ] @@ -87,7 +99,8 @@ rule AddPublicKey: * an invariant portion and a variant portion. This * allows tamarin to immediately bind the keys back * to this initial pairing rule. The fresh ~id is used - * to identify this pairing. */ + * to identify this pairing. We cache the SiSr in the + * invariant to reduce Tamarin's variant precomputation time. */ State(~id, 'no_message_state') , !StateInvariants(~id, ~psk, ~ltkA, pkB, pkB^~ltkA) ] @@ -110,7 +123,9 @@ rule Handshake_Init: ki2 = h(<ci1, sisr, '2'>) ats = aead(ki2, $ts, hi0) hi1 = h(<hi0, ats>) - m1 = <'1', ~sidI, pekI, astat, ats, $mac1, $mac2> in /* NOTE: MACs are currently not modeled. */ + /* NOTE: MACs used in the DDoS protection are not modeled, so we assume they are + * some arbitrary public values (i.e. known to the adversary, like a fixed string). */ + m1 = <'1', ~sidI, pekI, astat, ats, $mac1, $mac2> in [ /* 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. */ @@ -121,9 +136,12 @@ rule Handshake_Init: /* The pkISurrogate is used later to approximate identity hiding. */ , Fr(~pkISurrogate) ]--> - [ /* We cache DH sisr to reduce variant precomputation time for tamarin. */ - State(~id, <'init', ~sidI, ~ekI, ci2, ki2, hi1>) - , F_SolveInit(~id, ~psk, <'init', ~sidI, ~ekI, ci2, ki2, hi1>) /* HACK: This is a heuristic hack that should be removed. */ + [ State(~id, <'init', ~sidI, ~ekI, ci2, ki2, hi1>) + /* F_SolveInit is a bit of a hack to help with Tamarin's heuristics. It allows Tamarin to + * prioritize solving backwards from the Handshake_Complete rule even though the State + * fact is deprioritized by the m4 definitions above. This will not be necessary in a + * future version of Tamarin. */ + , F_SolveInit(~id, ~psk, <'init', ~sidI, ~ekI, ci2, ki2, hi1>) , !EphKeytoReveal(~ekI) , Out(m1) ] @@ -146,7 +164,7 @@ rule Handshake_Resp: kr2 = h(<cr1, sisr, '2'>) ats = aead(kr2, $ts, hr0) hr1 = h(<hr0, ats>) - m1 = <'1', sidI, pekI, astat, ats, $mac1, $mac2> /* NOTE: MACs are currently not modeled. */ + m1 = <'1', sidI, pekI, astat, ats, $mac1, $mac2> /* NOTE: MACs used in DDoS protection are not modeled. */ /* Constructing the response message m2: */ cr3 = h(<cr2, pekR, '1'>) hr2 = h(<hr1, pekR>) @@ -158,7 +176,7 @@ rule Handshake_Resp: hr3 = h(<hr2, hrt>) aempt = aead(kr6, 'e', hr3) hr4 = h(<hr3, aempt>) - m2 = <'2', sidI, ~sidR, pekR, aempt, $mac1, $mac2> in /* NOTE: MACs are currently not modeled. */ + m2 = <'2', sidI, ~sidR, pekR, aempt, $mac1, $mac2> in /* NOTE: MACs used in DDoS protection are not modeled. */ [ State(~id, anything) , !StateInvariants(~id, ~psk, ~ltkR, pkI, sisr) , Fr(~ekR) @@ -166,12 +184,13 @@ rule Handshake_Resp: , In(m1) ]--[ /* In the real protocol, this isn't actually cr6, but is rather derived from it - * via some more hashing, but it doesn't make a difference here. */ + * via some more hashing, but it doesn't make a difference here -- if the adversary knows cr6, + * it can compute the derived key. */ RKeys(<pkI, pkR, pekI, pekR, ~psk, cr6>) , Identity_Surrogate(pkISurrogate) ]-> [ State(~id, <'transport_unconfirmed', ~sidR, pekI, pekR, cr6>) - , F_SolveResp(~id, ~psk, <'transport_unconfirmed', ~sidR, pekI, pekR, cr6>) /* HACK: This is a heuristic hack that should be removed. */ + , F_SolveResp(~id, ~psk, <'transport_unconfirmed', ~sidR, pekI, pekR, cr6>) /* This is used for the same purpose as F_SolveInit above */ , !EphKeytoReveal(~ekR) , Out(m2) ] @@ -193,16 +212,16 @@ rule Handshake_Complete: aempt = aead(ki6, 'e', hi3) hi4 = h(<hi3, aempt>) m2 = <'2', sidI, sidR, pekR, aempt, $mac1, $mac2> - /* 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. */ + /* We assume the first transport message is 'as weak as possible', that is, all values + * in it are public other than the key used to encrypt. */ mtr = <'4', sidR, aead(ci6, 'message', '0')> in [ State(~id, <'init', sidI, ~ekI, ci2, ki2, hi1>) - , F_SolveInit(~id, ~psk, <'init', sidI, ~ekI, ci2, ki2, hi1>) /* HACK: This is a heuristic hack that should be removed. */ + , F_SolveInit(~id, ~psk, <'init', sidI, ~ekI, ci2, ki2, hi1>) , !StateInvariants(~id, ~psk, ~ltkI, pkR, sisr) , In(m2) ]--[ /* In the real protocol, this isn't actually ci6, but is rather derived from it - * via some more hashing, but it doesn't make a difference here. */ + * via some more hashing, but it doesn't make a difference here (as with cr6 above). */ IKeys(<pkI, pkR, pekI, pekR, ~psk, ci6>) ]-> [ State(~id, <'transport', sidI, ci6>) @@ -219,13 +238,13 @@ rule Handshake_Complete: rule R_ConfirmedTransportMessage: let mtr = <'4', sid, data> in [ State(~id, <'transport_unconfirmed', sidR, pekI, pekR, cr>) - , F_SolveResp(~id, ~psk, <'transport_unconfirmed', sidR, pekI, pekR, cr>) /* HACK: This is a heuristic hack that should be removed. */ + , F_SolveResp(~id, ~psk, <'transport_unconfirmed', sidR, pekI, pekR, cr>) , !StateInvariants(~id, ~psk, ~ltkR, pkI, sisr) , In(mtr) ]--[ RConfirm(<pkI, 'g'^~ltkR, pekI, pekR, ~psk, cr>) - //We manually verify this instead of the typical recomputation, since - //morally R may not know the contents of 'data'. + //We manually verify this instead of the recomputation used for other terms above, since + //morally R may not know the contents of the message. , Eq(verify(data, '0', cr), true) ]-> [ State(~id, <'transport', sidR, cr>) ] |