Attempt at modeling opportunistic Diffie-Hellman in Tamarin
theory Sean | |
begin | |
builtins: diffie-hellman | |
section{* DH *} | |
/* Opportunistic Diffie-Hellman */ | |
// Using ephemeral keys as thread identifiers | |
rule Initiator_1: | |
let epkI = 'g'^~eskI in | |
[ Fr( ~eskI ) ] | |
--> | |
[ Out( epkI ) | |
, Init( ~eskI ) | |
, !Ephemeral( ~eskI ) ] | |
rule Responder: | |
let epkR = 'g'^~eskR | |
kR = epkI^~eskR | |
in | |
[ In( epkI ), Fr( ~eskR ) ] | |
--[ Accept( ~eskR, kR ), Sid( ~eskR, <'Resp', epkI, epkR> ), Match( ~eskR, <'Init', epkI, epkR> ) ]-> | |
[ Out( epkR ) | |
, !Session( ~eskR, kR ) | |
, !Ephemeral( ~eskR ) ] | |
rule Initiator_2: | |
let kI = epkR^eskI | |
epkI = 'g'^eskI | |
in | |
[ In( epkR ), Init( eskI ) ] | |
--[ Accept( eskI, kI ), Sid( eskI, <'Init', epkI, epkR> ), Match( eskI, <'Resp', epkI, epkR>) ]-> | |
[ !Session( eskI, kI ) ] | |
/* Key Reveals */ | |
rule Ephemeral_reveal: | |
[ !Ephemeral( esk ) ] --[ EphemeralReveal( esk ) ]-> [ Out( esk ) ] | |
rule Session_reveal: | |
[ !Session( esk, k ) ] --[ SessionReveal( esk ) ]-> [ Out( k ) ] | |
// Secrecy of session keys | |
lemma session_key_secrecy: | |
"(All esk k #i #j. | |
( | |
// If the adversary knows the session key of session esk | |
(Accept( esk, k ) @ i & K( k ) @ j) | |
==> | |
// Then either... | |
( | |
// The session key has been revealed | |
(Ex #i2. SessionReveal( esk ) @ i2) | |
| // Or the session key of a matching session has been revealed | |
(Ex tid #i3 #i4 ms. | |
Sid ( tid, ms ) @ i3 | |
& Match( esk, ms ) @ i4 | |
& (Ex #i5. SessionReveal( tid ) @ i5) | |
) | |
| // Or the ephemeral key of the session has been revealed | |
(Ex #i6. EphemeralReveal( esk ) @ i6) | |
| // Or the ephemeral key of a matching session has been revealed | |
(Ex tid #i7 #i8 ms. | |
Sid ( tid, ms ) @ i7 | |
& Match( esk, ms ) @ i8 | |
& (Ex #i9. EphemeralReveal( tid ) @ i9) | |
) | |
) | |
) | |
)" | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment