Opportunistic Diffie-Hellman input for Tamarin

opportunistic_DH_new_try.spthy

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