From aa78951e2c0a23851c25055ab164bf79e9c74b0a Mon Sep 17 00:00:00 2001 From: "Jason A. Donenfeld" Date: Mon, 8 May 2017 15:28:02 +0200 Subject: Style --- wireguard.m4 | 183 +++++++++++++++++++++++++++++++---------------------------- 1 file changed, 96 insertions(+), 87 deletions(-) diff --git a/wireguard.m4 b/wireguard.m4 index 8c8b073..98f0a2f 100644 --- a/wireguard.m4 +++ b/wireguard.m4 @@ -7,66 +7,70 @@ changecom() * Date: 2017 * Source: Original * Status: Basically complete? Use the 'i' heuristic to autoprove. + * + * TODO: + * - Implement identity hiding properly using observational equivalence. + * - Prove indistinguishability using observational equivalence. + * - Model ECDH(private, NULL) = NULL */ 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. +/* We're not going to model the nonce in the aead, since it's always 0 in the handshake. */ functions: aead/3, decrypt/2, verify/3, true/0 -//The plaintext can be recovered with the key +/* 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 +/* The authentication can be checked with the key and AAD */ equations: verify(aead(k,p,a),a,k) = true restriction Eq_testing: "All x y #i. Eq(x,y) @ i ==> x = y" restriction InEq_testing: "All x y #i. InEq(x,y) @ i ==> not(x = y)" -//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. +/* 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. */ dnl define(In, AuthenticatedMessage($*)) dnl define(Out, AuthenticatedMessage($*)) -//These defines are for the heuristic goal sorting. F_ indicates that the -//heuristic should prioritize solving it, which we use to solve for where -//agents got various constraints (like the keys, and key relationships) +/* These defines are for the heuristic goal sorting. F_ indicates that the + * heuristic should prioritize solving it, which we use to solve for where + * agents got various constraints (like the keys, and key relationships) */ define(AgentKey, F_AgentKey($*)) define(AgentPSK, F_AgentPSK($*)) define(StateInvariants, F_StateInvariants($*)) -// L_ indicates the heuristic should deprioritize solving the goal. In this -// 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. + +/* L_ indicates the heuristic should deprioritize solving the goal. In this + * 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. */ dnl define(State, L_State($*)) -//Pre-established trust relationships +/* Pre-established trust relationships */ restriction pairings_unique: "All id id2 ka kb #i #j. Paired(id,ka,kb) @ i & Paired(id2,ka,kb) @ j ==> #i = #j" -//Keygen is separate from pairing to allow keys to be paired -//more than once (if they were generated fresh in the pairing -//this would not be possible) +/* Keygen is separate from pairing to allow keys to be paired + * more than once (if they were generated fresh in the pairing + * this would not be possible */ rule AgentKeyGen: [ Fr(~ltk) ] --[DHKey(~ltk)]-> [!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 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. +/* Semi-malicious or ignorant agents might share a PSK with multiple + * parties, so we'll overapproximate this by allowing it to be shared + * 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: [ Fr(~psk) ] --[PSKey(~psk)]-> [ !AgentPSK(~psk) ] -//Key Reveals for our adversary model +/* Key Reveals for our adversary model */ rule PSK_reveal: [ !AgentPSK(k) ] --[ Reveal_PSK(k) ]-> [ Out(k) ] @@ -76,9 +80,9 @@ rule AgentKey_reveal: rule EphKey_reveal: [ !EphKeytoReveal(k) ] --[ Reveal_EphK('g'^k) ]-> [ Out(k) ] -//Models an agent adding anothers public key out-of-band, we assume that -//all relationships set up this way are 'sane' and both of the keys involved -//were generated fresh. +/* Models an agent adding anothers public key out-of-band, we assume that + * all relationships set up this way are 'sane' and both of the keys involved + * were generated fresh. */ rule AddPublicKey: let pkB = 'g'^~ltkB in [ !AgentKey(~ltkA) @@ -86,21 +90,22 @@ rule AddPublicKey: , !AgentPSK(~psk) , Fr(~id) ]--> - [ // For search efficiency, state is divided into - // 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. + [ /* For search efficiency, state is divided into + * 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. */ State(~id,'no_message_state') , !StateInvariants(~id,~psk,~ltkA,pkB,pkB^~ltkA) ] -// MESSAGE RULES +/* === Message Rules === */ + rule Handshake_Init: let pkI = 'g'^~ltkI pekI = 'g'^~ekI eisr = pkR^~ekI - //Constructing the init message m1: + /* Constructing the init message m1: */ cii = h('noise') hii = h() ci0 = h() @@ -112,18 +117,18 @@ rule Handshake_Init: ki2 = h() ats = aead(ki2,$ts,hi0) hi1 = h() - m1 = <'1',~sidI,pekI,astat,ats,$mac1,$mac2> in //Note: MACs are currently not modeled - [ //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. + m1 = <'1',~sidI,pekI,astat,ats,$mac1,$mac2> in //NOTE: MACs are currently not modeled + [ /* 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,anything) , !StateInvariants(~id,~psk,~ltkI,pkR,sisr) , Fr(~sidI) , Fr(~ekI) - // The pkISurrogate is used later to approximate identity hiding. + /* The pkISurrogate is used later to approximate identity hiding. */ , Fr(~pkISurrogate) ]--> - [ //We cache DH sisr to reduce variant precomputation time for tamarin. + [ /* We cache DH sisr to reduce variant precomputation time for tamarin. */ State(~id,<'init',~sidI,~ekI,ci2,ki2,hi1>) , !EphKeytoReveal(~ekI) , Out(m1) @@ -135,7 +140,7 @@ rule Handshake_Resp: eisr = pekI^~ltkR eier = pekI^~ekR sier = pkI^~ekR - //Reconstructing what should be in m1: + /* Reconstructing what should be in m1: */ cri = h('noise') hri = h() cr0 = h() @@ -147,8 +152,8 @@ rule Handshake_Resp: kr2 = h() ats = aead(kr2,$ts,hr0) hr1 = h() - m1 = <'1',sidI,pekI,astat,ats,$mac1,$mac2> //Note: MACs are currently not modeled - //Constructing the response message m2: + m1 = <'1',sidI,pekI,astat,ats,$mac1,$mac2> //NOTE: MACs are currently not modeled + /* Constructing the response message m2: */ cr3 = h() hr2 = h() cr4 = h() @@ -159,15 +164,17 @@ rule Handshake_Resp: hr3 = h() aempt = aead(kr6,'e',hr3) hr4 = h() - m2 = <'2',sidI,~sidR,pekR,aempt,$mac1,$mac2> in + m2 = <'2',sidI,~sidR,pekR,aempt,$mac1,$mac2> in //NOTE: MACs are currently not modeled [ State(~id,anything) , !StateInvariants(~id,~psk,~ltkR,pkI,sisr) , Fr(~ekR) , Fr(~sidR) , In(m1) ]--[ - RKeys() //Not actually cr6, but derived from it. - , Identity_Surrogate(pkISurrogate) + /* 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. */ + RKeys() + , Identity_Surrogate(pkISurrogate) ]-> [ State(~id,<'transport_unconfirmed',~sidR,pekI,pekR,cr6>) , !EphKeytoReveal(~ekR) @@ -179,7 +186,7 @@ rule Handshake_Complete: pekI = 'g'^~ekI eier = pekR^~ekI sier = pekR^~ltkI - //Reconstruct what should be in m2: + /* Reconstruct what should be in m2: */ ci3 = h() hi2 = h() ci4 = h() @@ -191,26 +198,27 @@ rule Handshake_Complete: aempt = aead(ki6,'e',hi3) hi4 = h() 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 except the key used to encrypt. */ mtr = <'4',sidR,aead(ci6,'message','0')> in [ State(~id,<'init',sidI,~ekI,ci2,ki2,hi1>) , !StateInvariants(~id,~psk,~ltkI,pkR,sisr) , In(m2) ]--[ - IKeys() //Not actually ci6, but derived from it. + /* 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. */ + IKeys() ]-> [ State(~id,<'transport',sidI,ci6>) , Out(mtr) ] -///////////////////////////////////////////////////////////////////////////// -// Key confirmation (both modes) -// For proving agreement properties after the first transport message -// This is not faithfully modelled, since we don't care about the contents -// of the transport message--instead it's generically 'anything encrypted -// with the transport key I just set up' -///////////////////////////////////////////////////////////////////////////// +/* === Key Confirmation === + * + * For proving agreement properties after the first transport message + * This is not faithfully modelled, since we don't care about the contents + * of the transport message--instead it's generically 'anything encrypted + * with the transport key I just set up'. */ rule R_ConfirmedTransportMessage: let mtr = <'4',sid,data> in @@ -225,14 +233,16 @@ rule R_ConfirmedTransportMessage: ]-> [ State(~id,<'transport',sidR,cr>) ] +/* === Session Traces === + * + * We show that at least the protocol works. */ -///////////////////////////////////////////////////////////////////////////// lemma exists_session: exists-trace "Ex pki pkr peki pekr psk ck #i #j. IKeys() @ i & RConfirm() @ j & #i < #j" -//There are only three numbers, 0, 1, and infinity. So 2 == infinity +/* There are only three numbers, 0, 1, and infinity. So 2 == infinity */ lemma exists_two_sessions: exists-trace "Ex pki pkr sesskeys sesskeys2 #i #j #i2 #j2. IKeys() @ i @@ -241,41 +251,40 @@ lemma exists_two_sessions: exists-trace & #i < #i2 & not(sesskeys = sesskeys2)" -//////// AGREEMENT PROPERTIES /////////////////////////////////////////////// -// These all autoprove, though the first two take a while. -///////////////////////////////////////////////////////////////////////////// +/* === Agreement Properties === */ + lemma I_disagreement_implies_Sr_or_SiEi_compromise_and_PSK_compromise[reuse]: "All pki pkr peki pekr psk ck #i. - //If I believes they have completed a handshake with R + /* If I believes they have completed a handshake with R */ IKeys() @ i - //but R doesn't have a matching session + /* but R doesn't have a matching session */ & not(Ex #j. #j < #i & RKeys() @ j) - ==> //Then the PSK was compromised (or not in use) and + ==> /* Then the PSK was compromised (or not in use) and */ (Ex #j. Reveal_PSK(psk) @ j & #j < #i) & ( - //either R's static was compromised + /* either R's static was compromised */ (Ex #j. Reveal_AK(pkr) @ j & #j < #i) - //or both I's static and ephemeral were already compromised + /* or both I's static and ephemeral were already compromised */ | (Ex #j #j2. Reveal_AK(pki) @ j & #j < #i & Reveal_EphK(peki) @ j2 & #j2 < #i) )" lemma R_disagreement_implies_Si_or_SrEr_compromise_and_PSK_compromise[reuse]: "All pki pkr peki pekr psk ck #i. - //If R believes they have a confirmed session with I + /* If R believes they have a confirmed session with I */ RConfirm() @ i - //but I doesn't have a matching session + /* but I doesn't have a matching session */ & not(Ex #j. #j < #i & IKeys() @ j) - ==> //Then the PSK was compromised (or not in use) and + ==> /* Then the PSK was compromised (or not in use) and */ (Ex #j. Reveal_PSK(psk) @ j & #j < #i) & ( - //either I's static was compromised + /* either I's static was compromised */ (Ex #j. Reveal_AK(pki) @ j & #j < #i) - //or both R's static and ephemeral were already compromised + /* 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 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 - //RNG can be controlled instead of just revealed, which we do not model. + /* 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 + * RNG can be controlled instead of just revealed, which we do not model. */ "(All pki pkr peki pekr psk ck #i. IKeys() @ i ==> not(Ex peki2 pekr2 #k. IKeys() @ k & not(#k = #i))) @@ -283,33 +292,33 @@ lemma session_uniqueness: RConfirm() @ i ==> not(Ex peki2 pekr2 psk2 #k. RConfirm() @ k & not(#k = #i)))" -//////// SECRECY PROPERTIES ////////////////////////////////////////////////// -// All autoprove, but key_secrecy takes forever -///////////////////////////////////////////////////////////////////////////// +/* === Secrecy Properties === */ lemma key_secrecy[reuse]: "(All pki pkr peki pekr psk ck #i #i2. - //If I and R agree on keys + /* If I and R agree on keys */ IKeys() @ i & RKeys() @ i2 - ==> //Either the adversary doesn't know the keys + ==> /* Either the adversary doesn't know the keys */ not(Ex #j. K(ck) @ j) - //or the psk was compromised (or not in use) and pair of keys from the same agent was revealed (at any time) + /* or the psk was compromised (or not in use) */ | ((Ex #j. Reveal_PSK(psk) @ j) & ( + /* and pair of keys from the same agent was revealed (at any time) */ (Ex #j #j2. Reveal_AK(pki) @ j & Reveal_EphK(peki) @ j2) | (Ex #j #j2. Reveal_AK(pkr) @ j & Reveal_EphK(pekr) @ j2)) ))" lemma identity_hiding: - //Since the public static is always symbolically known to the adversary, we represent identity - //hiding by whether the adversary could learn some other value that is put in the first message at the - //same position as the public static. + /* Since the public static is always symbolically known to the adversary, we represent identity + * hiding by whether the adversary could learn some other value that is put in the first message at the + * same position as the public static. */ "All pki pkr peki pekr ck surrogate #i #j. - //If R received a handshake init with a particular identity surrogate + /* If R received a handshake init with a particular identity surrogate */ RKeys() @ i & Identity_Surrogate(surrogate) @ i - //And the adversary knows that surrogate for the identity + /* And the adversary knows that surrogate for the identity */ & K(surrogate) @ j - ==> //Then the adversary compromised at least one of R's static, I's static, or I's ephemeral + ==> /* 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)" + end // vim: ft=spthy -- cgit v1.2.3-59-g8ed1b