path: root/wireguard.m4

dnl // Tamarin uses ' which is an m4 close quote. So use <! !> for quoting instead.
changequote(<!,!>)
changecom(<!@,@!>)
/*
 * Protocol:    Wireguard protocol
 * Modeler: 	Kevin Milner
 * Date: 	    February 2017
 * Source:	    Original
 * Status: 	    WIP
 */

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. Note that this can only over-approximate attacks,
//since it would allow collisions between two AEADs with different nonces.
functions: aead/3, decrypt/2
equations: decrypt(aead(k,p,a),k) = p     //Plaintext can be recovered using the key

//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($*))

define(AgentKey, F_AgentKey($*))
define(StateInvariants, F_StateInvariants($*))

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)"

//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)
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.
rule PSKKeyGen:
    [ Fr(~psk) ]
    --[PSKey(~psk)]->
    [ !AgentPSK(~psk) ]

//Models an agent adding anothers public key out-of-band.
rule AddPublicKey:
    let pkB = 'g'^~ltkB in
    [ !AgentKey(~ltkA)
    , !AgentKey(~ltkB)
    , Fr(~id)
    ]--[
      InEq($A,$B)
    ]->
    [ // 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.
      State(~id, 'nopsk', 'nostate')
    , !StateInvariants(~id, ~ltkA, pkB, pkB^~ltkA)
    ]

/* Uncomment to allow various key compromises
 rule CompromiseKey:
    [!AgentKey(ltk)]
    --[ CompromiseLTK(ltk) ]->
    [Out(ltk)]

rule CompromisePSK:
    [!AgentPSK(psk)]
    --[ CompromisePSK(psk) ]->
    [Out(psk)]
*/

// MESSAGE RULES
rule Handshake_Init:
    let pkI   = 'g'^~ltkI
        pekI  = 'g'^~ekI
        eisr  = pkR^~ekI
        //Constructing the init message m1:
        cii   = h('nopsk')
        hii   = h(<cii,'id',pkR,pekI>)  //No PSK means no intermediate hashes necessary here
        ki0   = h(<cii,eisr,'2'>)
        ci0   = h(<cii,eisr,'1'>)
        astat = aead(ki0,pkI,hii)
        hi0   = h(<hii,astat>)
        ki1   = h(<ci0,sisr,'2'>)
        ci1   = h(<ci0,sisr,'1'>)
        ats   = aead(ki1,~ts,hi0)
        hi1   = h(<hi0,ats>)
        m1    = <'1',~sidI,pekI,astat,ats,$mac1,$mac2> in //TODO:Model MACs
    [ //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)
    , !StateInvariants(~id, ~ltkI, pkR, sisr)
    , Fr(~sidI)
    , Fr(~ekI)
    , Fr(~ts)
    ]--[
      StartHandshake(pkI,pkR,pekI,'nopsk',~sidI)
    ]->
    [ //We cache DH sisr to reduce variant precomputation time for tamarin.
      State(~id,'nopsk',<'init',~sidI,~ekI,ci1,ki1,hi1>)
    , Out(m1)
    ]

rule Handshake_Resp:
    let pkR   = 'g'^~ltkR
        pekR  = 'g'^~ekR
        eisr  = pekI^~ltkR
        eier  = pekI^~ekR
        sier  = pkI^~ekR
        //Reconstructing what should be in m1:
        cri   = h('nopsk')
        hri   = h(<cri,'id',pkR,pekI>)  //No PSK means no intermediate hashes necessary here
        kr0   = h(<cri,eisr,'2'>)
        cr0   = h(<cri,eisr,'1'>)
        astat = aead(kr0,pkI,hri)
        hr0   = h(<hri,astat>)
        kr1   = h(<cr0,sisr,'2'>)
        cr1   = h(<cr0,sisr,'1'>)
        ats   = aead(kr1,ts,hr0)
        hr1   = h(<hr0,ats>)
        m1    = <'1',sidI,pekI,astat,ats,$mac1,$mac2> //TODO:Model MACs
        //Constructing the response message m2:
        hr2   = h(<hr1,pekR>)
        kr2   = h(<cr1,eier,'2'>)
        cr2   = h(<cr1,eier,'1'>)
        kr3   = h(<cr2,sier,'2'>)
        cr3   = h(<cr2,sier,'1'>)
        aempt = aead(kr3,'0',hr2)
        hr3   = h(<hr2,aempt>)
        m2    = <'2',sidI,~sidR,pekR,aempt,$mac1,$mac2> in
    [ State(~id,'nopsk',anything)
    , !StateInvariants(~id,~ltkR,pkI,sisr)
    , Fr(~ekR)
    , Fr(~sidR)
    , In(m1)
    ]--[
      RKeys(<pkI,pkR,pekI,pekR,'nopsk',cr3>) //Not actually cr3, but derived from it.
    , RSessionID(sidI,~sidR)
    ]->
    [ State(~id,'nopsk',<'transport',cr3>)
    , Out(m2)
    ]

rule Handshake_Complete:
    let pkI   = 'g'^~ltkI
        pekI  = 'g'^~ekI
        eier  = pekR^~ekI
        sier  = pekR^~ltkI
        //Reconstruct what should be in m2:
        hi2   = h(<hi1,pekR>)
        ki2   = h(<ci1,eier,'2'>)
        ci2   = h(<ci1,eier,'1'>)
        ki3   = h(<ci2,sier,'2'>)
        ci3   = h(<ci2,sier,'1'>)
        aempt = aead(ki3,'0',hi2)
        hi3   = h(<hi2,aempt>)
        m2    = <'2',sidI,sidR,pekR,aempt,$mac1,$mac2> in
    [ State(~id,'nopsk',<'init',sidI,~ekI,ci1,ki1,hi1>)
    , !StateInvariants(~id,~ltkI,pkR,sisr)
    , In(m2)
    ]--[
      IKeys(<pkI,pkR,pekI,pekR,'nopsk',ci3>) //Not actually ci3, but derived from it.
    , ISessionID(sidI,sidR)
    ]->
    [ State(~id,'nopsk',<'transport',ci3>)
    ]

/////////////////////////////////////////////////////////////////////////////
//      PSK Mode 
// Switching mode interrupts any handshakes in progress (is this correct?)
/////////////////////////////////////////////////////////////////////////////

rule SwitchtoPSK:
    [ State(~id, 'nopsk', state)
    , !StateInvariants(~id,~ltkA,pkB,sisr)
    , !AgentPSK(~psk)
    ]--[
      AddPSK(~id,~psk)
    , InEq(state,'pskremoved') // Just so it doesn't loop forever here
    ]->
    [ State(~id,~psk,'pskadded')
    ]

rule RemovePSK:
    [ State(~id,~psk,anything)
    , !AgentPSK(~psk)
    ]--[
      RemovePSK(~id,~psk)
    ]->
    [ State(~id,'nopsk','pskremoved')
    ]

// MESSAGE RULES WITH PSK
rule Handshake_InitPSK:
    let pkI   = 'g'^~ltkI
        pekI  = 'g'^~ekI
        eisr  = pkR^~ekI
        //Construct init message m1:
        cii   = h(<'psk'>)
        cipsk = h(<cii,~psk,'1'>)
        kipsk = h(<cii,~psk,'2'>)
        hii   = h(<cipsk,'id',kipsk,pkR,pekI>)
        ci0   = h(<cipsk,pekI,'1'>)
        ki0   = h(<cipsk,pekI,'2'>)
        hi0   = h(<hii,pekI>)
        ci1   = h(<ci0,eisr,'1'>)
        ki1   = h(<ci0,eisr,'2'>)
        astat = aead(ki1,pkI,hi0)
        hi1   = h(<hi0,astat>)
        ci2   = h(<ci1,sisr,'1'>)
        ki2   = h(<ci1,sisr,'2'>)
        ats   = aead(ki2,~ts,hi1)
        hi2   = h(<hi1,ats>)
        m1    = <'1',~sidI,pekI,astat,ats,$mac1,$mac2> in //TODO:Model MACs
    [ //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,~psk,anything)
    , !StateInvariants(~id,~ltkI,pkR,sisr)
    , !AgentPSK(~psk)
    , Fr(~sidI)
    , Fr(~ekI)
    , Fr(~ts)
    ]--[
      StartHandshake(pkI,pkR,pekI,~psk,~sidI)
    , UsingPSK(~psk)
    ]->
    [ //We cache DH sisr to reduce variant precomputation time for tamarin.
      State(~id,~psk,<'init',~sidI,~ekI,ci2,ki2,hi2>)
    , Out(m1)
    ]

rule Handshake_RespPSK:
    let pkR   = 'g'^~ltkR
        pekR  = 'g'^~ekR
        eisr  = pekI^~ltkR
        eier  = pekI^~ekR
        sier  = pkI^~ekR
        //Reconstruct init message m1 to validate it
        cri   = h(<'psk'>)
        crpsk = h(<cri,~psk,'1'>)
        krpsk = h(<cri,~psk,'2'>)
        hri   = h(<crpsk,'id',krpsk,pkR,pekI>)
        cr0   = h(<crpsk,pekI,'1'>)
        kr0   = h(<crpsk,pekI,'2'>)
        hr0   = h(<hri,pekI>)
        cr1   = h(<cr0,eisr,'1'>)
        kr1   = h(<cr0,eisr,'2'>)
        astat = aead(ki1,pkI,hr0)
        hr1   = h(<hr0,astat>)
        cr2   = h(<cr1,sisr,'1'>)
        kr2   = h(<cr1,sisr,'2'>)
        ats   = aead(kr2,~ts,hi2)
        hr2   = h(<hr1,ats>)
        m1    = <'1',sidI,pekI,astat,ats,$mac1,$mac2> //TODO:Model MACs
        //Constructing the response message m2:
        cr3   = h(<cr2,pekR,'1'>)
        kr3   = h(<cr2,pekR,'2'>)
        hr3   = h(<hr2,pekR>)
        cr4   = h(<cr2,eier,'1'>)
        kr4   = h(<cr2,eier,'2'>)
        cr5   = h(<cr2,sier,'1'>)
        kr5   = h(<cr2,sier,'2'>)
        aempt = aead(kr5,'0',hr3)
        hr5   = h(<hr3,aempt>)
        m2    = <'2',sidI,~sidR,pekR,aempt,$mac1,$mac2> in
    [ State(~id,~psk, anything)
    , !StateInvariants(~id,~ltkR,pkI,sisr)
    , !AgentPSK(~psk)
    , Fr(~ekR)
    , Fr(~sidR)
    , In(m1)
    ]--[
      RKeys(<pkI,pkR,pekI,pekR,~psk,cr5>) //Not actually cr, but derived from it.
    , UsingPSK(~psk)
    , RSessionID(sidI,~sidR)
    ]->
    [ State(~id,~psk,<'transport',cr3>)
    , Out(m2)
    ]

rule Handshake_CompletePSK:
    let pkI   = 'g'^~ltkI
        pekI  = 'g'^~ekI
        eier  = pekR^~ekI
        sier  = pekR^~ltkI
        //Reconstructing the response message m2 to validate it
        ci3   = h(<ci2,pekR,'1'>)
        ki3   = h(<ci2,pekR,'2'>)
        hi3   = h(<hi2,pekR>)
        ci4   = h(<ci2,eier,'1'>)
        ki4   = h(<ci2,eier,'2'>)
        ci5   = h(<ci2,sier,'1'>)
        ki5   = h(<ci2,sier,'2'>)
        aempt = aead(ki5,'0',hi3)
        hi5   = h(<hi3,aempt>)
        m2    = <'2',sidI,sidR,pekR,aempt,$mac1,$mac2> in
    [ State(~id,~psk,<'init',sidI,~ekI,ci2,ki2,hi2>)
    , !StateInvariants(~id,~ltkI,pkR,sisr)
    , !AgentPSK(~psk)
    , In(m2)
    ]--[
      IKeys(<pkI,pkR,pekI,pekR,~psk,ci5>) //Not actually ci, but derived from it.
    , UsingPSK(~psk)
    , ISessionID(sidI,sidR)
    ]->
    [ State(~id,~psk,<'transport',ci3>)
    ]

/////////////////////////////////////////////////////////////////////////////

lemma exists_session_nopsk: exists-trace
    "Ex pki pkr peki pekr ck #i #j.
        IKeys(<pki,pkr,peki,pekr,'nopsk',ck>) @ i 
        & RKeys(<pki,pkr,peki,pekr,'nopsk',ck>) @ j & #j < #i"

// The following two exists-trace lemmas take a very long time to
// autoprove, but can be proved by hand with a bit of patience.
// The heuristic is not well-suited to completing traces instead
// of ruling out attacks.
lemma exists_session_psk: exists-trace
    "Ex pki pkr peki pekr psk ck #i #j.
        IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i & UsingPSK(psk) @ i
        & RKeys(<pki,pkr,peki,pekr,psk,ck>) @ j & #j < #i"

//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
        & RKeys(<pki,pkr,sesskeys>) @ j & #j < #i
        & IKeys(<pki,pkr,sesskeys2>) @ i2 & RKeys(<pki,pkr,sesskeys2>) @ j2 & #j2 < #i2
        & #i < #i2 & not(sesskeys = sesskeys2)"

lemma key_secrecy:
    "(All pki pkr peki pekr ck #i.
        IKeys(<pki,pkr,peki,pekr,ck>) @ i ==> not(Ex #j. K(ck) @ j))
    &(All pki pkr peki pekr ck #i.
        RKeys(<pki,pkr,peki,pekr,ck>) @ i ==> not(Ex #j. K(ck) @ j))"

lemma agreement[reuse]:
    "All keys #i.
        IKeys(keys) @ i ==> Ex #j. #j < #i & RKeys(keys) @ j"

//This follows immediately from agreement, since the agreed ck includes 
//at least one fresh term
lemma injective_agreement_I:
    "All pki pkr peki pekr ck #i #j.
        IKeys(<pki,pkr,peki,pekr,ck>) @ i & RKeys(<pki,pkr,peki,pekr,ck>) @ j
    ==> not(Ex peki2 pekr2 #k. RKeys(<pki,pkr,peki2,pekr2,ck>) @ k & not(#k = #j))"

end

// vim: ft=spthy