Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Opportunistic Diffie-Hellman input for Tamarin
theory Diffie_Hellman
begin
builtins: diffie-hellman
//
// Rules
//
rule client_init:
let pubKey = 'g'^~privKey
in
[Fr(~privKey)]
--[]->
[InitClient(~privKey, pubKey), Out(pubKey)]
rule server_response:
[Fr(~privKey), In(clientPubKey)]
--[SessionCreateServer(clientPubKey^~privKey)]->
[Out('g'^~privKey), Session(clientPubkey^~privKey)]
rule client_receive:
[InitClient(~privKey, pubKey), In(serverPubKey)]
--[SessionCreateClient(serverPubKey^~privKey)]->
[Session(serverPubKey^~privKey)]
rule terminate:
[Session(A)]
-->
[]
//
// Lemmas
//
// just making sure it works
lemma ExchangeWorks:
exists-trace
"Ex S #i #j. SessionCreateClient(S) @ #i & SessionCreateServer(S) @ #j & #j < #i & not(Ex #k. K(S) @ #k)"
lemma RecoverSessionKeyImpossible:
"All S #i #j. (SessionCreateClient(S) @ #i & SessionCreateServer(S) @ #j & #j < #i) ==> not(Ex #k. K(S) @ #k)"
lemma MITMImpossible:
"All S1 S2 #i #j. (SessionCreateClient(S1) @ #i & SessionCreateServer(S2) @ #j & #j < #i) ==> not(Ex #k1 #k2. K(S1) @ #k1 & K(S2) @ #k2)"
//
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment