Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
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