Confusing Message Derivation Check Failure with SAPIC+

[Daniel Zimmerman]

Hi, all! 

In attempting to specify some protocols using global state in SAPIC+, I tried the following very simple one:

theory test_state begin

let reader(state) = (

lock state;

lookup state as x in

event Read(state, x);

insert state, 'new';

unlock state

)

process:(

new state;

lock state;

insert state, 'old';

unlock state;

(

!reader(state)

)

)

lemma ExOld:

exists-trace

"Ex s x #i. Read(s, x)@i & x = 'old'"

lemma ExNew:

exists-trace

"Ex s x #i. Read(s, x)@i & x = 'new'"

lemma AlwaysOldOrNew:

"All s x #i. Read(s, x)@i ==> x = 'old' | x = 'new'"

end

I then ran tamarin-prover --prove on it, and all of the lemmas were proven... but it also reported a failed message derivation check, namely:

  The variables of the following rule(s) are not derivable from their premises, you may be performing unintended pattern matching.

Rule lookupstateasx_0_1111111: 

Failed to derive Variable(s): x.1

The translated rule in question is:

rule (modulo E) lookupstateasx_0_1111111[color=#408048,

process="lookup state.1 as x.1", issapicrule]:

[ State_1111111( lock, lock.1, state.1 ) ]

--[ IsIn( state.1, x.1 ) ]->

[ State_11111111( lock, lock.1, state.1, x.1 ) ]

So I'm not sure what exactly to make of this; is it something to worry about, or just an artifact of how SAPIC+ state lookup translation works?

Thanks in advance for any help.

-Dan ZImmerman

[Felix Linker]

Hi Dan,

I helped implement this feature. Let me describe you by example what it does. Presume you model a protocol using a hash-function and you include the following rule: [ In(h(x)) ] —> [ Out(x) ]. This rule inverts the hash-function which is generally impossible. The wellformedness check that raises an error for you tries to catch such issues.

However, depending on your exact model, there can also be situations where pattern matching like that is valid or required. The warning does look like an artifact of translation as the rule uses x.1 in its conclusions but not in its premise. I don’t know SAPIC+, however, so I cannot say that with certainty. In either case: if you’re certain that your model is correct, you can safely ignore the warning.

You can also deactivate this check by passing --derivcheck-timeout=0 as an option.

Happy proving, and best,

Felix

--
You received this message because you are subscribed to the Google Groups "tamarin-prover" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tamarin-prove...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tamarin-prover/fd7d2752-ad19-4ff7-8952-3653404ebcd8n%40googlegroups.com.