Monkey See, Monkey Prove.

As I was winding down active work on my Kintsugi project last year, I asked my supervisor what good next steps would be. One proposed avenue was to formally verify Kintsugi’s security, since the paper relies only on pen-and-paper intuition. This is how I learned about Tamarin, a prover for security protocols.

I’m enamoured by this idea of guaranteeing the safety of systems. There’s something incredibly satisfying about knowing a protocol is formally, mathematically, and exhaustively impassable. Providing this level of confidence is rare. Tamarin is especially interesting because it can untangle cryptography primitives like symmetric encryption and Diffie-Hellman. This means it can precisely track what an adversary can derive, finding issues with delicate interaction chains that are difficult to come up with otherwise. The invariant proving is also (mostly) automatic after writing the protocol model, so no need to do the math manually.

This automatic bit is important, because I lack enough experience to make much progress otherwise. My work with formal methods so far has mostly managed to sidestep the actual specification process. It was never in the scope of past projects, and part of it was also just pure intimidation by arcane syntax and principles. I think it’s a little embarrassing to call myself a researcher interested in formal verification if I haven’t done any of said verification, though, so I wanted to address this year. As we rang in the New Year, I set a resolution to learn Tamarin and take a stab at modelling something non-trivial.

My goal was to model basic Shamir Secret Sharing and Oblivious Pseudo-Random Functions, before moving onto Dynamic Proactive Secret Sharing and Threshold OPRFs. Finally, I would Frankenstein the models together to get a Kintsugi proof. Going further, there’s a similar protocol Juicebox that’s more or less Kintsugi-but-production-ready, so I thought I’d be able to contribute towards a formal model of that as well.

You’ll see in the rest of this post how lofty those goals were. I’ll cover the progress I’ve been able to make so far, including a brief explainer of Tamarin and the WIP models as they stand. Along the way, I’ll point out some of the obstacles and limitations I’ve encountered. Overall, I don’t think I had the right approach for Tamarin, nor perhaps was it the right fit for the job, but it was a great chance to learn a new tool regardless.

A Whirlwind Intro

It’s a bit hard to understand a post about learning Tamarin if I don’t explain its features. To start off, Tamarin is a tool for symbolic verification of security protocols. Symbolic means that no code is really being run. Instead, Tamarin works on abstract states. It’s a bit like those bad Facebook IQ game ads where they replace the numbers in an equation with pictures and symbols. In code, you might imperatively generate a message and hash it. From Tamarin’s perspective, it sees the message and the sender’s state as just some given circumstances. To continue the Facebook ad metaphor, say the message is a banana. Hashing it turns the banana into an apple: another state that doesn’t intrinsically mean anything to Tamarin. How do I relate my bananas and apples to get anything sensible?

99.999% of people can’t solve that puzzle, but Tamarin sure can. It does so by defining rules that dictate how to transition between these states. Some of these rules are built-in: for instance, rules for how encryption and Diffie-Hellman work. Others are user-defined: I can define that from a “haven’t sent anything” state, I can generate a random value and transition to a “have sent message X and now waiting for response” state. Humans do okay with defining their protocol’s happy path as a sequence of these state transitions, but we struggle with thinking of more roundabout attacks. Tamarin helps with figuring out if there’s combinations of states and extra computation that an attacker can do that can lead to unintended leaks. For example, while my protocol might assume a hashed message always came from an authenticated party, Tamarin’s built-in rules can derive that the attacker might also know the hashed version of a message. Tamarin really shines in more complicated interleavings of protocols where partial information from one run can benefit an attacker in another.

Tamarin uses the Dolev-Yao adversary model. This means the adversary can eavesdrop on, intercept, and interfere with messages sent over the network. It can also derive its own messages to send. However, it doesn’t have access to the internal computation within a state transition: it can grab the first banana message, and also the apple at the end, but doesn’t understand how the fruit metamorphed.

Enough of the abstract math with fruit, alas¹. Here’s an example of Tamarin syntax. The following example is my solution to the last of these Tamarin exercices. There are two parties, Alex and Blake. We’re getting Alex to generate a nonce and send it to Blake, who responds with their own nonce. Then, Alex generates a session key based on the two nonces and sends it to Blake. Bear with me:

theory ToyProtocol
begin

functions: kdf/3, mac/2

rule Init:
    [ Fr(~mk), Fr(~aid), Fr(~bid) ]--[ Init(~aid, ~bid, ~mk) ]->[ AState(~aid, 'INIT', ~mk), BState(~bid, 'INIT', ~mk) ]

rule AlexSendNonce:
    [ AState(~aid, 'INIT', ~mk), Fr(~anonce) ]--[ AlexSendNonce(~aid, ~mk, ~anonce) ]->[ AState(~aid, 'SENT_NONCE', <~mk, ~anonce>), Out(~anonce) ]

rule AlexSendNonceAgain:
    [ AState(~aid, 'SENT_NONCE', <~mk, ~anonce>) ]--[ AlexSendNonceAgain(~aid, ~mk, ~anonce) ]->[ AState(~aid, 'SENT_NONCE', <~mk, ~anonce>), Out(~anonce) ]

rule BlakeSendNonce:
    [ BState(~bid, 'INIT', ~mk), Fr(~bnonce), In(ANonce) ]--[ BlakeSendNonce(~bid, ~mk, ~bnonce) ]->[ BState(~bid, 'SENT_NONCE', <~mk, ANonce, ~bnonce>), Out(~bnonce) ]

rule AlexComputeSK:
    let
        SK = kdf(~mk, ~anonce, BNonce)
    in
    [ AState(~aid, 'SENT_NONCE', <~mk, ~anonce>), In(BNonce) ]--[ AlexComputeSK(~aid, ~mk, ~anonce, BNonce, SK) ]->[ AState(~aid, 'DONE', <~mk, ~anonce, BNonce, SK>), Out(mac(SK, 'ACK')) ]

rule BlakeComputeSK:
    let
        SK = kdf(~mk, Anonce, ~bnonce)
    in
    [ BState(~bid, 'SENT_NONCE', <~mk, Anonce, ~bnonce>), In(mac(SK, 'ACK')) ]--[ BlakeComputeSK(~bid, ~mk, Anonce, ~bnonce, SK) ]->[ BState(~bid, 'DONE', <~mk, Anonce, ~bnonce, SK>) ]

lemma HelperInitialNonce [reuse, use_induction]:
    "All mk aid anonce #i . AlexSendNonceAgain(aid, mk, anonce) @ #i ==> Ex #j . AlexSendNonce(aid, mk, anonce) @ #j & j < i"

lemma ProtocolCanComplete:
    exists-trace
        "Ex mk aid bid anonce bnonce sk #i #j . AlexComputeSK(aid, mk, anonce, bnonce, sk) @ #i & BlakeComputeSK(bid, mk, anonce, bnonce, sk) @ #j"

lemma AttackerCannotKnowBlake:
    "All mk bid anonce bnonce sk #i . BlakeComputeSK(bid, mk, anonce, bnonce, sk) @ #i ==> not (Ex #j. K(sk) @ #j)"

lemma AttackerCannotKnowAlex:
    "All mk aid anonce bnonce sk #i . AlexComputeSK(aid, mk, anonce, bnonce, sk) @ #i ==> not (Ex #j. K(sk) @ #j)"

lemma BlakeAfterAlex:
    "All mk bid anonce bnonce sk #i . BlakeComputeSK(bid, mk, anonce, bnonce, sk) @ #i ==> Ex aid #j . AlexComputeSK(aid, mk, anonce, bnonce, sk) @ #j & j < i"

end

Let’s first go over the protocol definition:

• The intended happy path is Init → AlexSendNonce → BlakeSendNonce → AlexComputeSK → BlakeComputeSK. If the network drops, we might need AlexSendNonceAgain to retry.
• The rules are the user-defined state transitions. They’re formatted like [Consumes]--[ActionDescription]->[Produces]. In the first rule, Init, I’m generating some random IDs and a master key with Fr() (“fresh”, which can be consumed immediately). I’m also producing the states AState and BState. These new states can only be consumed once — it’s like real-life bananas².
• The next rule, AlexSendNonce consumes the original AState and produces a new fresh nonce. It then creates another new AState — note that this is symbolically distinct from the first from Tamarin’s perspective. The <> indicates concatenation. Out() sends the nonce over the network. Importantly, in Tamarin’s attack model this means the attacker now has access to it.
• The BlakeSendNonce rule requires both the second AState after Alex’s sent his nonce and an initialized BState. Again, Blake sends his nonce via Out(), so the attacker also has access to this.
• AlexComputeSK uses a user-defined kdf function. In Tamarin, these functions are used to abstract computation. By default, these functions can also be executed by the adversary. Think general well-known operations like a hash: I (or an adversary) can use sha256 from any computer, but unless I know the underlying text I won’t learn anything new. Here, even though anonce and bnonce were exposed on the network, the adversary doesn’t know mk, so being able to apply the kdf isn’t helpful. Likewise, Alex sends his ACK message wrapped in a mac function. Otherwise, Tamarin’s adversary would be able to forge their own ACK messages.
• BlakeComputeSK checks Blake’s BState and the incoming message. Tamarin supports pattern matching (e.g. In(mac(SK, 'ACK'))) that lets Blake check the MAC is valid before accepting this state.

Onto the lemmas:

• These function not on the LHS or RHS of each rule, but on the state transition itself. Lemmas use the action facts: the bit inside the middle group in each rule. These action facts describe transition metadata so we can construct traces of possible executions and prove properties over them.
• Let’s skip the first lemma for now and look at ProtocolCanComplete. This is classic first-order logic: there’s a trace where there Exists some combination of variables such that AlexComputeSK and BlakeComputeSK can be reached. #i and #j are timestamps in Tamarin, and @ #i means some action fact occurred at time i.
• AttackerCannotKnowAlex and AttackerCannotKnowBlake are almost identical. They say that for All instances of BlakeComputeSK, there does not Exist any timestamp, at any possible point in the execution, where the attacker Knows the secret key.
• BlakeAfterAlex says that if BlakeComputeSK happened at time i, then there must have been a previous time j where AlexComputeSK happened, denoted by j < i at the end.
• We now have some properties we think are true. We then need to boot up Tamarin with tamarin-prover --interactive ., click each lemma, and choose one of the methods to prove it. I won’t go into more detail how to use the proof system. It’s very powerful, but I got by with just spamming a for autoprove. I’ve been assuming if Tamarin can’t autoprove my basic lemmas that it’s a case of PEBKAC.

We skipped the HelperInitialNonce lemma earlier, but it’s very important. Without it, Tamarin won’t actually terminate. Notice that we allow Alex to send retries (AlexSendNonceAgain). When Tamarin tries to prove something about the transition between Alex sending his nonce and Blake replying, Tamarin searches through its rules and tries to work backward from what could have happened. Hm, maybe we got to Blake’s reply by Alex resending his nonce. And maybe we got to that resend by Alex resending his nonce again. And again — this goes into infinity. We can help Tamarin by adding a small lemma that says we must bottom out this recursion somewhere, and that Alex must have first sent his nonce with the first rule before it was ever resent. We mark this lemma reuse so Tamarin knows to use it in proving other lemmas, and add use_induction because it’s a helpful strategy for these “infinite recursion” situations.

Counting is Hard

As my first step to specifying Kintsugi, I wanted to specify the secret sharing (you can read more about it here). I’d already cut scope and started with basic SSS instead of DPSS. There are a few Tamarin specs of secret sharing-like protocols out there, and in particular I was inspired by abstractions from this one. However, I couldn’t find any that were generic in the number of participants: all of them used hardcoded rules based on three or so nodes. I was expecting something TLA+-like, where I could define a general model, and separately, a config file that set the limits of how many nodes I wanted. Unfortunately, this turns out to be really ugly in Tamarin (if you’d like, expand the dropdown to view the theory).

theory SSS
begin

builtins: natural-numbers

functions: gen_share/1 // simulating executing SSS polynomial S(i) on the index i

predicates: LessThan(x,y) <=> x ⊏ y,
GreaterThan(x,y) <=> y ⊏ x

rule Constants:
[]-->[ !Nval(%1%+%1%+%1%+%1%+%1), !Kval(%1%+%1%+%1) ] // best way I've found to define numerical constants

rule InitDealer:
[]--[ InitDealer() ]->[ DealerInit(%1) ]

rule InitOneNode:
let
// should really be gen_share(%counter) but functions can't be defined over nats
share = gen_share(~id)
in
[ Fr(~id), !Nval(%n), DealerInit( %counter) ]--[ InitOneNode(~id, %counter), _restrict(LessThan(%counter, %n %+ %1)) ]->[ !NodeState(~id, share), DealerInit( %counter %+ %1), Out(share) ]

rule InitCount:
[ Fr(~count_token) ]--[ InitCount(~count_token) ]->[ Collector(~count_token, %1) ]

rule DoCount:
[ Collector(~count_token, %counter), !NodeState(~id, share) ]--[ DoCount(~count_token, %counter), Counted(~count_token, ~id) ]->[ Collector(~count_token, %counter %+ %1) ]

rule DoLastCount:
[ !Kval(%k), Collector(~count_token, %counter) ]--[ DoLastCount(~count_token, %k %+ %1), _restrict(GreaterThan(%counter, %k)) ]->[ !SSSPoly() ]

rule DeriveSecret:
// s is supposed to be derived from the polynomial, but can't model the lagrange interpolation
[ !Kval(%k), !SSSPoly(), Fr(~s) ]--[ DeriveSecret(~s), !Kval(%k) ]->[ !SSSSecret(~s) ]

restriction NoDoubleCount:
"All count_token id #i #j. Counted(count_token,id)@i & Counted(count_token,id)@j ==> #i = #j"

lemma sss_secret:
"All s %k ct #i #j #l .
!Kval(%k) @ #i &
DoLastCount(ct, %k %+ %1) @ #j &
DeriveSecret(s) @ #l &
#i < #j & #j < #l
==>
not (Ex #m . K(s) @ #m & #m < #l)" // s is not known before final derivation rule, which requires k threshold values

end

This initial experiment taught me three main things about Tamarin. First, some raw crypto math can’t be directly expressed in Tamarin. For example, SSS requires doing division and subtraction, but subtraction isn’t supported in Tamarin. Tamarin does have an inv for multiplication (i.e. it supports division, x * inv(x) = 1), but SSS additionally requires an inverse for addition. As such, I had to abstract the math at a much higher level, using a blanket SSSPoly() state and dummy shares.

Second, writing out raw numbers is really annoying in Tamarin. I wanted to make my model generic in the number of nodes. However, I can’t just write %3, it’s got to be %1%+%1%+%1%. In some ways this makes sense: to go back to the math with fruit analogy, Tamarin just sees bananas and apples. All rules, like adding up constants from the basic %1, have to be encoded explicitly for it to understand what “three” means in apple terms. This friction is probably a good sign I’m not thinking at the right level of abstraction, but surely I should be allowed to have small constants in my theories? I did find a solution: if you look at the Constants rule in my theory, you’ll see that I have persistent facts for Nval and Kval because I got tired of rewriting all the %s. This lets me access the constants using a more comfortable %n and %k syntax in the other rules.

Third, loops are also unwieldy. In SSS, each node has to collect at least k shares before it can reconstruct the polynomial. In an imperative language, this is a simple loop, but Tamarin is a glorified state machine. In my model, this loop translates to a rule that initializes the count of shares this node has (InitCount), another that increments the count (DoCount), and the final rule that exits the loop to the last state (DoLastCount, which results in the SSS polynomial being revealed). I trigger the DoLastCount with an action restriction (the _restrict) that only enables this rule when we’ve counted at least k shares already. I technically think it’s possible the DoCount keeps looping, but this didn’t cause any problems with Tamarin proving my final lemma. I’ll also note that loops in Tamarin necessarily have to count up, since there’s no such thing as subtraction!

All in all, the current SSS proof is quite unsatisfying, as it feels too abstract and relies on the Lagrange/math proofs being encoded elsewhere. The lack of Tamarin natural-numbers operations means the “secret” is “derived” very trivially (and is unrelated in Tamarin’s universe to the actual polynomial). I wrestled with the math so long last year and had wanted some more solid validation. However, given the hoops I’d already had to jump through to specify a basic loop, I didn’t think I could figure out how to express the basis polynomials in Tamarin.

Knowledge is Power

I then tried specifying an OPRF (read more about them here). I thought this would be easier, since there’s less finicky math and Tamarin has support for the group operations I’d need. Also, basic OPRFs have more structured client-server communication, which I thought would align better with Tamarin’s abstractions. You can see my final model in the dropdown.

theory OPRF
begin

builtins: diffie-hellman, symmetric-encryption

rule InitClient:
[ Fr(~id), Fr(~s), Fr(~r) ]--[ InitClient(~id, ~s, ~r) ]->[ CState(~id, ~s, ~r), Out(<'blinded', ('g' ^ ~s) ^ ~r>) ]

rule InitServer:
[ Fr(~k) ]--[ InitServer(~k), OnlyOnce() ]->[ !SState(~k) ]

rule SendResponse[no_derivcheck]:
let
res = 'g' ^ pow
bk = res ^ ~k
in
[ !SState(~k), In(<'blinded', res>) ]--[ DoesNotKnow(pow), SendResponse(~k, res) ]->[ Out(<'blinded_key', bk>) ]

rule ComputeRwd[no_derivcheck]:
let
res = 'g' ^ pow
rwd = res ^ inv(~r)
ee = senc(~kp, rwd)
in
[ Fr(~kp), CState(~id, ~s, ~r), In(<'blinded_key', res>) ]--[ DoesNotKnow(pow), ComputeRwd(~id, ~s, ~r, rwd, ~kp) ]->[ !CStateFinal(~id, ~s, ~kp), Out(<'ee', ~id, ee>) ]

rule StoreEncryptedEnvelope:
[ In(<'ee', ~id, ee>) ]--[ StoreEncryptedEnvelope(~id, ee) ]->[ !EncryptedEnvelope(~id, ee) ]

restriction only_once:
"All #i #j . OnlyOnce() @ #i & OnlyOnce() @ #j ==> #i = #j"

restriction does_not_know:
"All pow #i. DoesNotKnow(pow) @#i ==> not (Ex #j . K(pow) @ #j & #j < #i)"

lemma protocol_can_complete:
exists-trace
"Ex id s r ee #i #j . InitClient(id, s, r) @ #i & StoreEncryptedEnvelope(id, ee) @ #j & #i < #j"

lemma oprf_secrecy:
"
All id s r k rwd kp ee #a #b #c .
InitServer(k) @ #a &
ComputeRwd(id, s, r, rwd, kp) @ #b &
StoreEncryptedEnvelope(id, ee) @ #c &
#a < #b & #b < #c
==>
not (Ex #d . K(k) @ #d) &
not (Ex #d . K(s) @ #d) &
not (Ex #d . K(r) @ #d)
"

end

The math was indeed easier with this theory: it was straightforward to modify the OPRF to work “in the exponent” since I only had one operation to invert. Here, I was able to make use of Tamarin’s Diffie-Hellman primitives. In all the 'g' ^ pow operations above, 'g' represents the base and the single quotes denote that 'g'’s public knowledge.

While writing this theory, I confronted one of the Tamarin beasts I haven’t yet mentioned: partial deconstructions. These happen because Tamarin starts processing our theory by looking through all the premises (LHSes) of our rules. Then, Tamarin tries to look back to see what could have caused that rule. Partial deconstructions denotes that it couldn’t figure out where something came from. This is due to some of Tamarin’s typing limitations, but is usually resolvable. The easy way is to pass --auto-sources to tamarin-prover, which will try to generate a sources lemma that describes where facts could have come from. The hard way if autosources isn’t sufficient is to write a sources lemma yourself, proving for all occurrences of the problematic action, either an attacker knew the value beforehand or it came from the valid happy path source. The hard way is a bit intimidating, but the manual’s guide is helpful enough.

In my case, the prover could not for the life of it understand that it couldn’t just learn res ^ ~k in SendResponse. I spent while trying to write my own sources lemma to combat this, but I was limited in where math can be used. I couldn’t use exponents in the sources lemma, nor could I define my own inv function and equational theory (which also couldn’t be used in the sources lemma anyways). In theory given the hardness of the DLP I could model exponentiation as an extra secret function to prevent the prover from further exploring that path, but that felt counter to the spirit of specifying the OPRF.

However, as a maintainer then kindly pointed out, if the partial deconstruction is due to some intermediate combination of variables, like res ^ ~k, it doesn’t help to prove a sources lemma on either res or ~k. In this case, pattern matching was the solution: instead of receiving some generic variable in, I could force it to, say, 'g'^exp. I don’t think this is a general fix, but in my case this was enough to get Tamarin to understand where the value was coming from. One slight hitch, though, was that this creates an unbounded variable exp. To prevent Tamarin compiler errors, we need to annotate the rule with no_derivcheck. This disables the check that the attacker cannot gain extra capabilities; namely, that it cannot derive exp. Consider this a Chekhov’s gun for later (a Chekhov’s banana?).

Binary Search Debugging

I was able to prove the final lemma that the OPRF secrets indeed remain secret and was feeling more accomplished at this point. Given that this lemma proves the secrecy of k, s, and r, then, surely it’d be easy to also extend the lemma to ensure the secrecy of the shared secret rwd = 'g' ^ k ^ s. So I wrote the following lemma:

lemma oprf_secrecy_rwd:
"
All id s r k rwd kp #a #b .
InitServer(k) @ #a &
ComputeRwd(id, s, r, rwd, kp) @ #b &
#a < #b
==>
not (Ex #c . K(rwd) @ #c)
"

Unfortunately, Chekhov’s gun comes back: this fails to prove. It’s not that it finds a counterexample, just that it keeps running forever.

Once upon a time a scholarship mentor taught me about binary-search debugging: if a program fails, take out half of it and see if the failure persists. If not, you’ve narrowed it down to the other half, and so on. I tried to apply the same philosophy to this OPRF model, varying the levels of computation and number of messages exchanged as my search criteria. I wrote three other variants of the OPRF model, even cutting down the communication to sending just a single message across and unblinding it with a shared key. So far, I’ve come to the conclusion that if I have a single message between client and server, with a single exponentiation and no_derivcheck, I can prove a secrecy lemma. If I send a blinded message, apply an exponent, then receive and unblind the response (two messages between client and server), the prover hangs.

This probably points at a loop somewhere where the no_derivcheck is allowing for some infinite state to be accumulated. I don’t know Tamarin well enough to diagnose this directly, and the in-progress diagrams didn’t show any clear loops. I’ve tried adding extra action restrictions, but model checking still chewed up all my memory. Maybe my machine isn’t beefy enough, maybe (probably) my model is off. It’s an unsatisfying result, but this is as far as I got at the end of a month on-and-off and my patience.

Conclusion

I came into this experiment with high expectations of what Tamarin would help me prove, but my takeaway is that it’s harder to work with than expected.

I admit this is a bit of a captious take given my lack of Tamarin experience, but I haven’t been able to wrap my mental models into Tamarin’s view of how things should work. Maybe it’d get better if I stuck with it and tried modelling simpler protocols. Up to now, though, the word that keeps coming to mind is unsatisfying, mostly in terms of the abstractions I’m able to use. I think it’s valid criticism that a beginner user who puts in an earnest effort into learning a prover should feel more empowered than I did. For example, this is the first time model checking state space explosion has been a real issue, but the manual doesn’t have much hand-holding to explain how to debug. Tamarin’s walls come up pretty fast, and from there it’s hard to figure out how to exit the maze. In general, this also demonstrates to me why formal methods adoption is so low, given how intimidating and opaque it can be.

I think one thing TLA+ does better in comparison is in onboarding folks used to “normal” imperative development. There’s PlusCal, which provides a conceptual stepping stone, and more examples of how common puzzles a user’s likely heard of (Tower of Hanoi, Goats and Cabbages) can be expressed in TLA+. This makes it more comfortable to ease into TLA+’s model of states and invariants and so on. The examples in Tamarin’s manual are quite advanced protocols — I was expecting more toy Alice and Bob situations rather than Naxos and Needham-Schroeder-Lowe, for example.

Another interesting point is that Tamarin is not very GPT-able, unlike TLA+. This wipes out an easy source of debugging help. ChatGPT tends to get Tamarin syntax wrong, confusing the action rule arrows, and doesn’t understand Tamarin’s restricted models any better than I do. Of course, this is expected due to the relative lack of Tamarin examples in the training data, but is still a practical consideration. I once brought Tamarin up with a researcher at a large American AI company, but given its relative lack of popularity, I doubt any official fine-tuning will come of it. From a user’s perspective, there are still techniques one might try to get better Tamarin results from stock models, like providing a BNF grammar or loading the manual as docs for an agent to explore. I do think agents’ reasoning capabilities would be sufficient to help with the core security thinking, but the Tamarin abstractions are just not transparent enough for models to intuit the basic semantics.

I don’t mean to dog on Tamarin: it’s a really neat tool and research direction. I plan on going through the new book sometime, which I suspect will be an enormous help. In the meantime, though, I’m thinking of retrying this experiment in another theorem prover to see if Kintsugi and my mental models fit better with another paradigm. I’m debating between ProVerif and Squirrel. I’m leaning towards the latter as it postdates both Tamarin and ProVerif and because of a nice compelling video. Surely keeping up with the mammalian prover trend will get me somewhere.