Skip to content

Instantly share code, notes, and snippets.

@Phasip

Phasip/Tamarin Counter Loop Bug

Created March 17, 2015 06:20
Show Gist options
  • Save Phasip/cb531f887deeff5f5146 to your computer and use it in GitHub Desktop.
Save Phasip/cb531f887deeff5f5146 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Tamarin Counter Loop Bug
theory Loop_Counter_Test begin
functions: inc/1
rule Start: [ Fr(x) ] --[ ]-> [ A(x,x) ]
rule Loop: [ A(x,y) ] --[ Loop(x,y) ]-> [ A(x,inc(y)) ]
lemma Exists:
exists-trace
"Ex #i x y. Loop(x,inc(y)) @ #i"
lemma Loop_inc [reuse]:
"All x y #j. Loop(x,inc(y)) @ #j ==>
(Ex #i. Loop(x,y) @ #i & #i = #j)"
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment