Bug Related to Injective Facts and Tuple Unfolding

[niklasmedinger]

Bug Report

Unfortunately, there currently is a bug related to injective facts and their monotone, (strictly) decreasing, (strictly) increasing positions in Tamarin. The bug occurs because of how the behavior of a position is turned into constraints on the terms in this position during constraint solving. Concretely, wrong constraints are added which can lead to Tamarin discarding valid traces. We have created a minimal example of the bug where it occurs because the model uses tuples inside an injective fact and only pattern-matches this tuple in some of the rules but not all.

This bug first manifested in this commit, and was merged into the develop/master branch here. Thus, all Tamarin versions since July last year were affected.

The Minimal Example

This is the minimal example we identified:

theory test_inj_tuple_bug
begin

/*
   Protocol:    Example
   Modeler:     Cas Cremers, Niklas Medinger
   Date:    July 2024

   Status:  working

 */

rule Init:
  [ Fr(~x) ] --[ C(~x) ]-> [ S(~x,<'a1','a2'>) ]

rule Update_Var:
  [ S(~x,D) ] --[ A(~x,D) ]->
  [ S(~x,D) ] 

lemma possible[use_induction]:
  exists-trace
  "Ex id x y z #i1 #i2 . A(id,x)@i1 & A(id,<y,z>)@i2 "

end

Tamarin can find a trace for versions prior to the buggy commit but not after. This includes the current develop and master branch.

This is the output of current develop Tamarin.

(I don't know why Tamarin claims I have uncommited changes. As you can see by the green checkmark in the terminal, my git repo is clean, and I just built Tamarin prior to running the model.)

This is the output of the version directly before the buggy commit was applied.

I've already investigated this bug quite a bit and will open a pull request immediately.

The Bug in a Nutshell

Tamarin tries to compute the behavior (constant/(strictly) increasing/(strictly) decreasing) for positions inside of injective facts. When the top-level fact is a tuple, it unfolds this tuple (in a particular way) to also reason about positions within the tuple. During constraint solving, Tamarin uses the behavior of these terms to add additional constraints. However, the unfolding logic during constraint solving differs from the unfolding during the behavior computation. As a result, constraints on the wrong terms are added which leads to Tamarin discarding valid traces.

To fix the bug, we simply need to make the unfolding logic in InjectiveFactInstances.hs and Simplify.hs consistent.

The Bug in More Detail

This section contains my personal notes I took during investigating the bug. It is not well formatted or structured, and might contain mistakes. I'll post it here so people who are interested in learning more about the bug or Tamarin can read them. Enjoy!

---

We will now describe the bug in more detail, starting with when and where it manifests.

When a Tamarin model contains an injective fact, it computes whether terms inside this fact are monotone, (strictly) increasing, or (strictly) decreasing. In the following, assume S is injective.

Example 1:

rule Update_Var:
  [ S(~x,a, b) ] --[ A(~x,a, b) ]->
  [ S(~x,a, h(b)) ] 

Tamarin will correctly compute that S is injective, monotone in a, and strictly increasing in b. In the GUI, one can check this by clicking on Multiset rewriting rules where it will be displayed like this: S(id, =, <).

A somewhat common pattern is to use a tuple inside of an injective fact to model dynamic state for this fact. E.g., S(~x, <a, b>) -> S(~x, <a, c>). For cases like this, position 2 of S is not constant, but 2.1 is.

Intuitively, Tamarin could detect this by flattening the tuples into a list and checking whether the zipped lists of terms from the lhs and rhs of a rule shows any behavior.

Example 2:

rule Update_Tuple:
  [ S(~x,<a, b>) ] --[ A(~x,<a, b>) ]->
  [ S(~x,<a, b>) ] 

Here, Tamarin could compute [[=], [=]] for S at position 2 because [[a, a], [b, b]] is constant in each pair. This works fine for a single rule, but is not that easy for multiple rules because only some of them might pattern match the tuple; other rules might not. We will not outline how Tamarin computes the shape of a term in a top-level positions to approximate the behavior of the term in all rules.

The shape of a top-level term (line 109, InjectiveFactInstances.hs) is the list that you get by flattening tuples into its left term and recursively flattening the right term until you encounter a non-tuple term. E.g., the shape of <<a, b>, c> is [<a, b>, c], the shape of a is [a], and the shape of <a, <b, c>, d> is [a, <b, c>, d]. In the actual code, shape is again [[MonotonicBehaviour]] because it considers a whole fact instead of terms at a specific position. Next, the shapes of top-level terms in the same position of an injective fact are combined by taking zipping them together (line 114). Assume that the shape of S at position p in rule i is [<a, b>, c] and in rule j it is [a]. I.e, rule i uses pattern matching on the tuple and rule j simply copies a variable. Then, zip [<a, b>, c] [a] = [a], and thus the shape of S at position p is [a]. In a nutshell, the smallest common denominator of pattern matching that all rules use is just a variable. The shape is now used to compute the behavior of top-level terms in all of the rules in a model.

Example 3:

rule Intro:
  [ Fr(~x) ] -->
  [ S(~x,<<'a', 'b'>, 'c'>) ] 

rule Update_Var:
  [ S(~x,a) ] -->
  [ S(~x,a) ] 

rule Update_Tuple:
  [ S(~x,<<a, b>, c>) ] -->
  [ S(~x,<<b, b>, c>) ] 

Here, the shape of S--in position 2--in Update_Var is [a] and in Update_Tuple it is [<a, b>, c]. Thus, the combined shape of S at position 2 in the model is [a].

The length of the shape of position i of an injective fact S is now used to compute the behavior of S in i by only unzipping less than the length. E.g., for shape [a] at position 2 from Example 3, we compare [(a, a)] in rule Update_Var and [(<<a, b>, c>, <<b, b>, c>)] to get the behavior S(id, .). The left term of the tuple comes from the lhs instance of S and the right one form the rhs. Because the length of [a] is one, we don't unzip any tuples. Another example.

Example 4:

rule Intro:
  [ Fr(~x) ] -->
  [ S(~x,<<'a', 'b'>, <'c', 'd'>>) ] 

rule Update_Var:
  [ S(~x,<a, b>) ] -->
  [ S(~x,<a, b>) ] 

rule Update_Tuple:
  [ S(~x,<<a, b>, <c, d>>) ] -->
  [ S(~x,<<b, b>, <c, d>>) ] 

Again, we consider position 2 for S. The shape in Update_Var is [a, b]. The shape in Update_Tuple is [a, b, c, d]. The combined shape is [a, b] with length two. Thus, we flatten tuples once and consider terms [(a, a), (b, b)] for Update_Var with behavior [(=), (=)], and terms [(<a, b>, <b,b>), (<c, d>, <c, d>)] for Update_Tuple with behavior [(.), (=)] (note: . stands for unstable behavior). The combined behavior of S is thus S(id, (., =)).

The bug is now caused because the constraint solving logic does not respect the computed shape of terms. Instead, it eagerly flattens all tuples it encounters (line 610, Simplify.hs). Consider Example 3 with behavior [=] again. If we have two fact instances of S(~x, a) and S(~x, <b, c>), the logic in simpInjectiveFactEqMon will eagerly flatten <b, c> into [b, c] and a into [a]. Then, it will falsely apply the behavior [=] to these lists adding the equation a = b. Instead, it should not have flattened <b, c> and added the equation a = <b, c>.

[cascremers]

Thanks for the explanation and fix -- just accepted the PR.