Today I received a bug report from Tom Roeder, in which he demonstrated that...
Today I received a bug report from Tom Roeder, in which he demonstrated that the following models, Model A and Model B, caused a crash in Verifpal. Let’s look at Model A: ``` // Model A attacker[active] principal Client[ knows private a, b, c, d, e, f gg = CONCAT(a, b, c) h = CONCAT(gg, d, e) ] Client -> Server : h principal Server[ gc, dc, ec, fc = SPLIT(h) ac, bc, cc = SPLIT(gc) ] queries[ authentication? Client -> Server: h ] ``` Here, the cause is obvious: `h` is being split into four values despite being comprised of a concatenation of three values. This should not crash Verifpal, but should reasonably either be defined behavior or throw an error. However, if we look at Model B: ``` // Model B attacker[active] principal Client[ knows private a, b, c, d, e, f gg = CONCAT(a, b, c) h = CONCAT(gg, d, e, f) ] Client -> Server : h principal Server[ gc, dc, ec, fc = SPLIT(h) ac, bc, cc = SPLIT(gc) ] queries[ authentication? Client -> Server: h ] ``` Here Verifpal crashes despite the model being sane. This is because the active attacker renders it non-sane by replacing `h` with CONCAT(any, three, values), again triggering the crash when `h` is split into four values despite being a concatenation of three values. Thus Tom showed that the bug caused a crash in Verifpal in both non-sane (Model A) and sane (Model B) models. At this point, it became clear that it was important to clearly define Verifpal’s behavior when faced with such instances. I have decided to define it such that any extraneous values are rewritten to `nil`. So, for example, in Model A, on this line: ``` gc, dc, ec, fc = SPLIT(h) ``` `fc` will be rewritten to the `nil` value. This seems to be the most sensible defined behavior for this sort of scenario.