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