summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorJason A. Donenfeld <Jason@zx2c4.com>2017-05-08 16:10:51 +0200
committerJason A. Donenfeld <Jason@zx2c4.com>2017-05-08 16:16:00 +0200
commitd6ff336b332df53521bd8d9aec6d09e9eaf4fdd2 (patch)
tree45aa71f5a31a33035d5d82a227596efc38a54996
parentStyle (diff)
downloadwireguard-tamarin-d6ff336b332df53521bd8d9aec6d09e9eaf4fdd2.tar.xz
wireguard-tamarin-d6ff336b332df53521bd8d9aec6d09e9eaf4fdd2.zip
Be less ugly
-rw-r--r--wireguard.m4168
1 files changed, 84 insertions, 84 deletions
diff --git a/wireguard.m4 b/wireguard.m4
index 98f0a2f..661ea06 100644
--- a/wireguard.m4
+++ b/wireguard.m4
@@ -21,12 +21,12 @@ builtins: hashing, diffie-hellman
/* 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 */
-equations: decrypt(aead(k,p,a),k) = p
+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
+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)"
+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
@@ -50,7 +50,7 @@ dnl define(State, L_State($*))
/* Pre-established trust relationships */
restriction pairings_unique:
"All id id2 ka kb #i #j.
- Paired(id,ka,kb) @ i & Paired(id2,ka,kb) @ j
+ Paired(id, ka, kb) @ i & Paired(id2, ka, kb) @ j
==> #i = #j"
/* Keygen is separate from pairing to allow keys to be paired
@@ -95,8 +95,8 @@ 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,'no_message_state')
- , !StateInvariants(~id,~psk,~ltkA,pkB,pkB^~ltkA)
+ State(~id, 'no_message_state')
+ , !StateInvariants(~id, ~psk, ~ltkA, pkB, pkB^~ltkA)
]
/* === Message Rules === */
@@ -107,29 +107,29 @@ rule Handshake_Init:
eisr = pkR^~ekI
/* Constructing the init message m1: */
cii = h('noise')
- hii = h(<cii,'id',pkR,pekI>)
- ci0 = h(<cii,pekI,'1'>)
- ci1 = h(<ci0,eisr,'1'>)
- ki1 = h(<ci0,eisr,'2'>)
- astat = aead(ki1,<pkI,~pkISurrogate>,hii)
- hi0 = h(<hii,astat>)
- ci2 = h(<ci1,sisr,'1'>)
- 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
+ hii = h(<cii, 'id', pkR, pekI>)
+ ci0 = h(<cii, pekI, '1'>)
+ ci1 = h(<ci0, eisr, '1'>)
+ ki1 = h(<ci0, eisr, '2'>)
+ astat = aead(ki1, <pkI, ~pkISurrogate>, hii)
+ hi0 = h(<hii, astat>)
+ ci2 = h(<ci1, sisr, '1'>)
+ 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
[ /* 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)
+ State(~id, anything)
+ , !StateInvariants(~id, ~psk, ~ltkI, pkR, sisr)
, Fr(~sidI)
, Fr(~ekI)
/* 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>)
+ State(~id, <'init', ~sidI, ~ekI, ci2, ki2, hi1>)
, !EphKeytoReveal(~ekI)
, Out(m1)
]
@@ -142,41 +142,41 @@ rule Handshake_Resp:
sier = pkI^~ekR
/* Reconstructing what should be in m1: */
cri = h('noise')
- hri = h(<cri,'id',pkR,pekI>)
- cr0 = h(<cri,pekI,'1'>)
- cr1 = h(<cr0,eisr,'1'>)
- kr1 = h(<cr0,eisr,'2'>)
- astat = aead(kr1,<pkI,pkISurrogate>,hri)
- hr0 = h(<hri,astat>)
- cr2 = h(<cr1,sisr,'1'>)
- 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
+ hri = h(<cri, 'id', pkR, pekI>)
+ cr0 = h(<cri, pekI, '1'>)
+ cr1 = h(<cr0, eisr, '1'>)
+ kr1 = h(<cr0, eisr, '2'>)
+ astat = aead(kr1, <pkI, pkISurrogate>, hri)
+ hr0 = h(<hri, astat>)
+ cr2 = h(<cr1, sisr, '1'>)
+ 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
/* Constructing the response message m2: */
- cr3 = h(<cr2,pekR,'1'>)
- hr2 = h(<hr1,pekR>)
- cr4 = h(<cr3,eier,'1'>)
- cr5 = h(<cr4,sier,'1'>)
- cr6 = h(<cr5,~psk,'1'>)
- hrt = h(<cr5,~psk,'2'>)
- kr6 = h(<cr5,~psk,'3'>)
- 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
- [ State(~id,anything)
- , !StateInvariants(~id,~psk,~ltkR,pkI,sisr)
+ cr3 = h(<cr2, pekR, '1'>)
+ hr2 = h(<hr1, pekR>)
+ cr4 = h(<cr3, eier, '1'>)
+ cr5 = h(<cr4, sier, '1'>)
+ cr6 = h(<cr5, ~psk, '1'>)
+ hrt = h(<cr5, ~psk, '2'>)
+ kr6 = h(<cr5, ~psk, '3'>)
+ 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
+ [ State(~id, anything)
+ , !StateInvariants(~id, ~psk, ~ltkR, pkI, sisr)
, Fr(~ekR)
, Fr(~sidR)
, 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. */
- RKeys(<pkI,pkR,pekI,pekR,~psk,cr6>)
+ RKeys(<pkI, pkR, pekI, pekR, ~psk, cr6>)
, Identity_Surrogate(pkISurrogate)
]->
- [ State(~id,<'transport_unconfirmed',~sidR,pekI,pekR,cr6>)
+ [ State(~id, <'transport_unconfirmed', ~sidR, pekI, pekR, cr6>)
, !EphKeytoReveal(~ekR)
, Out(m2)
]
@@ -187,29 +187,29 @@ rule Handshake_Complete:
eier = pekR^~ekI
sier = pekR^~ltkI
/* Reconstruct what should be in m2: */
- ci3 = h(<ci2,pekR,'1'>)
- hi2 = h(<hi1,pekR>)
- ci4 = h(<ci3,eier,'1'>)
- ci5 = h(<ci4,sier,'1'>)
- ci6 = h(<ci5,~psk,'1'>)
- hit = h(<ci5,~psk,'2'>)
- ki6 = h(<ci5,~psk,'3'>)
- hi3 = h(<hi2,hit>)
- aempt = aead(ki6,'e',hi3)
- hi4 = h(<hi3,aempt>)
- m2 = <'2',sidI,sidR,pekR,aempt,$mac1,$mac2>
+ ci3 = h(<ci2, pekR, '1'>)
+ hi2 = h(<hi1, pekR>)
+ ci4 = h(<ci3, eier, '1'>)
+ ci5 = h(<ci4, sier, '1'>)
+ ci6 = h(<ci5, ~psk, '1'>)
+ hit = h(<ci5, ~psk, '2'>)
+ ki6 = h(<ci5, ~psk, '3'>)
+ hi3 = h(<hi2, hit>)
+ 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. */
- mtr = <'4',sidR,aead(ci6,'message','0')> in
- [ State(~id,<'init',sidI,~ekI,ci2,ki2,hi1>)
- , !StateInvariants(~id,~psk,~ltkI,pkR,sisr)
+ mtr = <'4', sidR, aead(ci6, 'message', '0')> in
+ [ State(~id, <'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. */
- IKeys(<pkI,pkR,pekI,pekR,~psk,ci6>)
+ IKeys(<pkI, pkR, pekI, pekR, ~psk, ci6>)
]->
- [ State(~id,<'transport',sidI,ci6>)
+ [ State(~id, <'transport', sidI, ci6>)
, Out(mtr)
]
@@ -221,17 +221,17 @@ rule Handshake_Complete:
* with the transport key I just set up'. */
rule R_ConfirmedTransportMessage:
- let mtr = <'4',sid,data> in
- [ State(~id,<'transport_unconfirmed',sidR,pekI,pekR,cr>)
- , !StateInvariants(~id,~psk,~ltkR,pkI,sisr)
+ let mtr = <'4', sid, data> in
+ [ State(~id, <'transport_unconfirmed', sidR, pekI, pekR, cr>)
+ , !StateInvariants(~id, ~psk, ~ltkR, pkI, sisr)
, In(mtr)
]--[
- RConfirm(<pkI,'g'^~ltkR,pekI,pekR,~psk,cr>)
+ 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'.
- , Eq(verify(data,'0',cr),true)
+ , Eq(verify(data, '0', cr), true)
]->
- [ State(~id,<'transport',sidR,cr>) ]
+ [ State(~id, <'transport', sidR, cr>) ]
/* === Session Traces ===
*
@@ -239,15 +239,15 @@ rule R_ConfirmedTransportMessage:
lemma exists_session: exists-trace
"Ex pki pkr peki pekr psk ck #i #j.
- IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i
- & RConfirm(<pki,pkr,peki,pekr,psk,ck>) @ j & #i < #j"
+ IKeys(<pki, pkr, peki, pekr, psk, ck>) @ i
+ & RConfirm(<pki, pkr, peki, pekr, psk, ck>) @ j & #i < #j"
/* 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(<pki,pkr,sesskeys>) @ i
- & RConfirm(<pki,pkr,sesskeys>) @ j & #i < #j
- & IKeys(<pki,pkr,sesskeys2>) @ i2 & RConfirm(<pki,pkr,sesskeys2>) @ j2 & #i2 < #j2
+ IKeys(<pki, pkr, sesskeys>) @ i
+ & RConfirm(<pki, pkr, sesskeys>) @ j & #i < #j
+ & IKeys(<pki, pkr, sesskeys2>) @ i2 & RConfirm(<pki, pkr, sesskeys2>) @ j2 & #i2 < #j2
& #i < #i2 & not(sesskeys = sesskeys2)"
@@ -256,9 +256,9 @@ lemma exists_two_sessions: exists-trace
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 */
- IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i
+ IKeys(<pki, pkr, peki, pekr, psk, ck>) @ i
/* but R doesn't have a matching session */
- & not(Ex #j. #j < #i & RKeys(<pki,pkr,peki,pekr,psk,ck>) @ j)
+ & not(Ex #j. #j < #i & RKeys(<pki, pkr, peki, pekr, psk, ck>) @ j)
==> /* Then the PSK was compromised (or not in use) and */
(Ex #j. Reveal_PSK(psk) @ j & #j < #i) & (
/* either R's static was compromised */
@@ -270,9 +270,9 @@ lemma I_disagreement_implies_Sr_or_SiEi_compromise_and_PSK_compromise[reuse]:
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 */
- RConfirm(<pki,pkr,peki,pekr,psk,ck>) @ i
+ RConfirm(<pki, pkr, peki, pekr, psk, ck>) @ i
/* but I doesn't have a matching session */
- & not(Ex #j. #j < #i & IKeys(<pki,pkr,peki,pekr,psk,ck>) @ j)
+ & not(Ex #j. #j < #i & IKeys(<pki, pkr, peki, pekr, psk, ck>) @ j)
==> /* Then the PSK was compromised (or not in use) and */
(Ex #j. Reveal_PSK(psk) @ j & #j < #i) & (
/* either I's static was compromised */
@@ -286,18 +286,18 @@ lemma session_uniqueness:
* 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(<pki,pkr,peki,pekr,psk,ck>) @ i
- ==> not(Ex peki2 pekr2 #k. IKeys(<pki,pkr,peki2,pekr2,psk,ck>) @ k & not(#k = #i)))
+ IKeys(<pki, pkr, peki, pekr, psk, ck>) @ i
+ ==> not(Ex peki2 pekr2 #k. IKeys(<pki, pkr, peki2, pekr2, psk, ck>) @ k & not(#k = #i)))
&(All pki pkr peki pekr psk ck #i.
- RConfirm(<pki,pkr,peki,pekr,psk,ck>) @ i
- ==> not(Ex peki2 pekr2 psk2 #k. RConfirm(<pki,pkr,peki2,pekr2,psk2,ck>) @ k & not(#k = #i)))"
+ RConfirm(<pki, pkr, peki, pekr, psk, ck>) @ i
+ ==> not(Ex peki2 pekr2 psk2 #k. RConfirm(<pki, pkr, peki2, pekr2, psk2, ck>) @ k & not(#k = #i)))"
/* === Secrecy Properties === */
lemma key_secrecy[reuse]:
"(All pki pkr peki pekr psk ck #i #i2.
/* If I and R agree on keys */
- IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i & RKeys(<pki,pkr,peki,pekr,psk,ck>) @ i2
+ IKeys(<pki, pkr, peki, pekr, psk, ck>) @ i & RKeys(<pki, pkr, peki, pekr, psk, ck>) @ i2
==> /* Either the adversary doesn't know the keys */
not(Ex #j. K(ck) @ j)
/* or the psk was compromised (or not in use) */
@@ -313,7 +313,7 @@ lemma identity_hiding:
* 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 */
- RKeys(<pki,pkr,peki,pekr,ck>) @ i & Identity_Surrogate(surrogate) @ i
+ RKeys(<pki, pkr, peki, pekr, ck>) @ i & Identity_Surrogate(surrogate) @ i
/* 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 */