tamarin-prover/tamarin-prover — pull request #138 by oggy- (2014-01-20 19:43:27+00:00)
Title: Reasoning about inductive facts ignores "last" formulas

Reasoning about injective facts requires three timepoints i, j, k, such that i < j < k. When last(k) holds, the temporal ordering between j and k is apparently implicit. Currently, this causes Tamarin to fail to derive a contradiction, even when one exists. An example follows (Tamarin fails to prove the lemma).

theory Last_Injective
begin

rule New_Loop:
[ Fr(~x) ]
--[ New_Loop(~x) ]->
[ Loop(~x, '1') ]

rule Start_Loop:
[ Loop(x, '1') ]
--[ Start_Loop(x) ]->
[ Loop(x, '2') ]

rule Do_Loop:
[ Loop(x, '2') ]
--[ In_Loop(x) ]->
[ Loop(x, '2') ]

rule Stop_Loop:
[ Loop(x, '2') ]
--[ Stop_Loop(x) ]->
[ Loop(x, '1') ]

lemma No_Stop_In_Loop[use_induction]:
"All x #i.
In_Loop(x) @ i ==> (
Ex #j. Start_Loop(x) @ j
& j < i
& (All #k. Stop_Loop(x) @ k ==> k < j | i < k)
)
"

end