Code to analyze the security of Diffie-Hellman with the Tamarin Solver

opportunistic_DH.spthy

theory Sean
begin

builtins: diffie-hellman

section{* DH *}

/* Generate ephemeral keypair */
rule generate_ephemeral:
   [ Fr(~secretk)] 
   -->
   [ Keys( ~secretk, 'g'^~secretk ) ]

/* protocol */
rule Init_client:
   [ Keys(~secretk, 'g'^~secretk) ]
   -->
   [ Keys(~secretk, 'g'^~secretk), Out( 'g'^~secretk ) ]

rule Init_Finish_server:
  let pubkey_other = 'g'^r
  in
   [ Keys(~secretk, 'g'^~secretk), In( pubkey_other ) ]
   --[ Session_created(pubkey_other^~secretk) ]->
   [ Session(pubkey_other^~secretk), Out( 'g'^~secretk ) ]

rule Finish_client:
  let pubkey_other = 'g'^r
  in
   [ Keys(~secretk, 'g'^~secretk), In( pubkey_other ) ]
   --[ Session_created(pubkey_other^~secretk) ]->
   [ Session(pubkey_other^~secretk) ]

/* Key Reveals */
rule key_reveal:
   [ Keys(~secretk, 'g'^~secretk) ]--[ Key_reveal(~secretk) ]-> [ Out(~secretk) ]

rule Session_reveal:
  [ Session(skey) ] --[ Reveal_sessionKey(skey)]-> [ Out(skey)]

// lemma
lemma session_key:

  "(All #i1 skey .
    (
      Session_created(skey) @ i1 
      &
      not ( (Ex A #ia . Key_reveal( A ) @ ia ) 
          | (Ex B #ib . Reveal_sessionKey( B ) @ ib )
          )
    )
    ==> not (Ex #i2. K( skey ) @ i2 )
  )"

end