Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Code to analyze the security of Diffie-Hellman with the Tamarin Solver
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment