Skip to content

Instantly share code, notes, and snippets.

@Phasip

Phasip/weird_axiom.spthy

Created February 25, 2015 08:14
Show Gist options
  • Save Phasip/444516a0316e6559c116 to your computer and use it in GitHub Desktop.
Save Phasip/444516a0316e6559c116 to your computer and use it in GitHub Desktop.
Download ZIP
Tamarin issue using axiom.
Raw
weird_axiom.spthy
theory BadTheory_axiom
begin
rule ProbablyBug:
[
Fr(~kenb)
]
--[
SessionKey(~kenb)
]->
[]
lemma secrecy:
"All k #i. SessionKey(k) @ i ==>
(not(Ex #j. K(k) @ j))"
axiom stupid_axiom:
"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