Attempt at modeling opportunistic Diffie-Hellman in Tamarin

opportunistic_DH.spthy

theory Sean
begin

builtins: diffie-hellman

section{* DH *}

/* Opportunistic Diffie-Hellman */

// Using ephemeral keys as thread identifiers
rule Initiator_1:
  let epkI = 'g'^~eskI in
  [ Fr( ~eskI ) ]
  -->
  [ Out( epkI )
  , Init( ~eskI )
  , !Ephemeral( ~eskI ) ]

rule Responder:
  let epkR = 'g'^~eskR
      kR = epkI^~eskR
  in
   [ In( epkI ), Fr( ~eskR ) ]
   --[ Accept( ~eskR, kR ), Sid( ~eskR, <'Resp', epkI, epkR> ), Match( ~eskR, <'Init', epkI, epkR> ) ]->
   [ Out( epkR )
   , !Session( ~eskR, kR )
   , !Ephemeral( ~eskR ) ]

rule Initiator_2:
  let kI = epkR^eskI 
      epkI = 'g'^eskI 
  in
   [ In( epkR ), Init( eskI ) ]
   --[ Accept( eskI, kI ), Sid( eskI, <'Init', epkI, epkR> ), Match( eskI, <'Resp', epkI, epkR>) ]->
   [ !Session( eskI, kI ) ]

/* Key Reveals */
rule Ephemeral_reveal:
  [ !Ephemeral( esk ) ] --[ EphemeralReveal( esk ) ]-> [ Out( esk ) ]

rule Session_reveal:
  [ !Session( esk, k ) ] --[ SessionReveal( esk ) ]-> [ Out( k ) ]

// Secrecy of session keys
lemma session_key_secrecy:
  "(All esk k #i #j.
    (
      // If the adversary knows the session key of session esk
      (Accept( esk, k ) @ i & K( k ) @ j)
      ==>
      // Then either...
      ( 
        // The session key has been revealed
        (Ex #i2. SessionReveal( esk ) @ i2)
      | // Or the session key of a matching session has been revealed
        (Ex tid #i3 #i4 ms.
            Sid ( tid, ms ) @ i3 
          & Match( esk, ms ) @ i4
          & (Ex #i5. SessionReveal( tid ) @ i5)
        )
      | // Or the ephemeral key of the session has been revealed
        (Ex #i6. EphemeralReveal( esk ) @ i6)
      | // Or the ephemeral key of a matching session has been revealed
        (Ex tid #i7 #i8 ms.
            Sid ( tid, ms ) @ i7 
          & Match( esk, ms ) @ i8
          & (Ex #i9. EphemeralReveal( tid ) @ i9)
        )
      )
    ) 
  )"

end