Skip to content

Instantly share code, notes, and snippets.

@Phasip
Created February 25, 2015 08:13
Show Gist options
  • Save Phasip/2c6a5aed307e3cb74f11 to your computer and use it in GitHub Desktop.
Save Phasip/2c6a5aed307e3cb74f11 to your computer and use it in GitHub Desktop.
Tamarin issue using typing lemma.
theory BadTheory_Typing
begin
rule ProbablyBug:
[
Fr(~kenb)
]
--[
SessionKey(~kenb)
]->
[NewKey(~kenb)] //Must be added for error with typing to appear
lemma secrecy:
"All k #i. SessionKey(k) @ i ==>
not(Ex #j. K(k) @ j)"
lemma stupid_lemma [typing]:
"All k #i. SessionKey(k) @ i ==>
Ex #j. SessionKey(k) @ j"
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment