path: root/transcripts/london-bitcoin-devs/2020-02-04-james-chiang-trace-net.mdwn

Name: James Chiang

Topic: Bitcoin Trace-Net

Location: London Bitcoin Devs

Date: February 4th 2020

Video: https://www.youtube.com/watch?v=SMvoGkxMyYs

Slides: https://www.dropbox.com/s/99md18bnnl8jnnw/James%20Chiang%20-%20Bitcoin%20Trace%20Net.pdf

# Intro

Good evening. My name is James and it is a real privilege to give this talk right after Andrew (Poelstra) has primed the entire audience on Miniscript. That’s pretty awesome. I learned a lot of things even though I coded the stuff that they have on Pieter’s website the actual justification and reasoning behind a lot of the decisions they made in the language were very insightful. I first heard about Miniscript during the summer of last year. I was at the residency at Chaincode. This website from Pieter popped up. The fact that you can now statically analyze the Bitcoin Script language was a real eye opener for me. Following that I had this thought that maybe given one can analyze all the satisfaction paths of an output it may be possible to verify a more complicated contracting protocol like Lightning or payment channels or coinjoins. In Ethereum you have a smart contract, it is this persistent object and you can call it multiple times. You can have all these state changes but it is still the same smart contract object. You can kind of analyze a Solidity contract with a lot of traditional software security methods because it is just a program that has state. You call it over and over again and there are these interesting transitions. But in Bitcoin a Script instance just has three states: unconfirmed, unspent confirmed and spent. Then it is done, there are no more state transitions that it can go through. When we construct protocols in Bitcoin we do it over parent-child transactions, atomic swaps where there are two transactions involved and they are atomically linked with a hashlock. The goal of this project that I have been working on for a couple of months is to find a modeling language which we can, with a tool like Miniscript, be able to model check any kind of protocol contract that you may want to use for interactive protocols. There is a paper that I submitted to CryptoEconSys which got accepted with a couple of notes for revision, the bulk of this presentation is based on that.

# Generalized key management

The basic motivation is the following. Today if you have Lightning or a coinjoin implementation the wallet signs specifically for that protocol. There is some kind of templating code that checks for the type of contract it is signing and it knows therefore when certain things can be done and when certain things can’t be done. For example if I have some kind of protocol and I first begin by generating Script locks. Script locks can be hashlocks, public keys, all these things that we use in interactive protocols. From those we then generate contract templates which must be signed and endorsed before the contract can begin. The question is can we have some kind of verification against a generalized signing policy? This signing policy might be “I’ll sign this contract if the implied balance is so and so.” We want to define a safety property of that contract that is generalizable across all contracts expressible in Bitcoin transactions and Bitcoin Script, in our case Miniscript because we constrain our use of Script to Miniscript. That’s the basic idea.

# Miniscript

This slide is to quickly recap Miniscript and why it is so useful especially in the case of contract verification. Given a Miniscript encoded output I can parse it for the different satisfaction paths and branches. Every satisfaction path is basically just a combination of different types of Script locks. It can be a public key, a hashlock, timelock or maybe some literal data you need to supply the witness with to unlock the output. That is nice because I can take a script or template transaction and I can kind of start modeling what possible satisfaction paths exist. I can generate some kind of state machine out of that contract.

Here is an example of an output O. That output O may have three satisfaction paths. This is just an example. We have one with time delay and a public key lock. Here is another time delay and a public key lock generated by Party B. We might have one which features two public keys generated by two parties. One output script, three satisfaction paths encoded by the witness encoding. This is something that you can automate with Miniscript.

# Definition: Contract Execution Trace

The basic goal is to say we have some kind of contract state and we want to define different types of transitions which capture all contract state transitions that can occur. I want to figure out whether I can reach a final state that is safe for the verifier. State being for example that I can withdraw the funds from the contract unilaterally. Another requirement for this trace is I want to make sure that the contract is designed in a way that I as the verifier can unilaterally execute this trace and this trace is robust against competing actions by the counterparty. If the counterparty can do something like race spend an output, the design of the contract needs to be robust and safe against that. Then we will see later on how we define that over the properties of the different traces. In the first step we want to define the different types of transitions and we want to define what a contract state actually is. Whether that is generalizable across any Bitcoin transaction written with Miniscript.

# Definition: Contract Actors

I call this modern language Trace-Net. In Trace-Net we distinguish between only twin actors. There may be more actors involved in the protocol but we initially distinguish between two. The reason is because the verifying Internal Actor will generate all these Script locks, pubkeys, hashlocks. The Internal Actor can only determine which Script locks it has satisfied and shared with the outside world. The Internal Actor can only determine which Script locks it itself has generated and their state. Their state is have I shared a preimage? Have I shared a signature? Have I shared for example a private key component? That is the only state the Internal Actor can trace. The Internal Actor cannot distinguish between multiple actors externally. It does not know whether two pubkeys were generated by two people or whether two parties controlled secrets to two public keys. We only have the Internal Actor and the External Actor. In the life cycle of a contract, let’s say a payment channel, we have the generation of the Script locks: pubkeys, hash digests. We have some kind of Contract Verification before we sign. Then we have Contract Updates. Updates can be we add a transaction template, we add a signature, I reveal a preimage as the contract life cycle continues. Those are the two actors that we have in this model.

# Definition: Contract Transition Types

I have defined three types of transitions. We have the off-chain transition which is basically just an exchange between actors. Exchanging sigs or preimages. Nothing is actually broadcast onchain. Then we have the actual onchain transition which has certain firing semantics that we will define in a second. This is when an actual transaction is broadcast and executed onchain. Then we have time transitions which are fired in specific cases. The time transitions allow us to respect the firing ordering enforced by timelocks. For the onchain transition I am going to use the classical Petri Net modeling language. That is something I extend on. The name Petri Net, I forget the guy who invented it, it is a modern language designed to model biochemical processes. That is where the Petri Net name comes from, from petri dish. It is very useful for modeling concurrent processes which may be competing for certain types of resources. The resource we are modeling here are unspent outputs.

# Off-chain transitions: e_sig, e_key, e_preimg

I’ll start with the offchain transition definition because that is the easiest one. Let’s say we have different Script locks. We have pubkeys, internally or externally generated pubkeys. We might have a shared pubkey. We might have hashlocks. You can see here that we have the Internal and External Actor. Depending on whether an offchain transition is fired the ability of that actor to produce that witness component changes. This is some kind of contract state that we are trying to express here. We have an internally generated public key. The Internal Actor can obviously produce the signature anytime. The External Actor can only produce it obviously if it was from the counterparty. That state changes from zero to one if this transition fires, if this offchain transition fires. Similarly if the internal hashlock generated by the Internal Actor, if the Internal Actor then shares the preimage with the counterparty then the counterparty now can produce that preimage as well. As the protocol proceeds these events take place. The ability of each actor to produce a specific witness element also changes. We want to be able to model that and that is what offchain transitions do. One thing I should note is that certain offchain transitions are implied by onchain transitions. Let’s say you have an onchain transition, a transaction being confirmed which features the unlocking of a hashlock. That obviously implies that an offchain transition can no longer fire. Once a piece of information is revealed, that’s a one time thing. Now we have these offchain events. Those are the firing rules. It can fire anytime but it can only fire once. Potentially it can be implied by an onchain transition especially if a hash digest is spent onchain.

Q - Can I just clarify on the External Actor? The External Actor cannot impact the state of the contract until they have become an Internal Actor?

A - The External Actor can definitely affect the state of the contract regardless of the Internal Actor.

Q - I thought that was how you defined it on the previous slide. They didn’t have a private key to sign for something?

A - I guess what I was trying to say there was there is only the Internal and External Actor because that is the only differentiation the Internal Actor can make. The Internal Actor can only determine this Script lock, do I control it or not? The Internal Actor cannot say “There are three Script locks. I control one and the other two are maybe controlled by two other parties.” There is no way that he, she or it can ascertain that. In this model it is the same actor. We had this conversation over lunch with ariard. For example you have HTLCs on both sides, receive and send. Those are two different actors I’m contracting with but in this model they are the same actor.

Q - You said that it is implied if it is onchain that you know it offchain? I guess you could throw in a wrench and say “We also want to take into account eclipse attacks.”

A - I don’t model that.

Q - You should take into account the mempool. If the transaction is in the mempool with a preimage, that is a transition.

A - I don’t think I differentiate between mempool and confirmation. Or eclipse attacks for that matter.

# “Classical” Petri Net

Let me quickly go through the firings for a classical net. We define our transition. Now we want to define the firing rules for the classical Petri Net skeleton that we use for this modeling language. There are a couple of things that we use. We have a Place. We have a Token. You can think of the Place as the Petri dish. We have Arcs and Transitions. A Token exists in a Place and can only exist in a Place. An Arc always points from a Place to a Transition or from a Transition to a Place. The direction of the Arc implies where the Token is being consumed from and where it goes. Here is an example. We have three Places. I have noted an index here 0, 1, 2. As you can see there is a Transition. The Transition can only fire if its pre-Places are populated. The pre-Place here is this Place here. In this state the transition can fire because its pre-Places are populated with the amount of Tokens that it needs. When it fires it produces Tokens to its destination Places. This basically models what an onchain transaction does. It takes unspent outputs and creates unspent outputs. That’s a one-to-one modeling that we have here. We need to overlay a little more state on top of it because we are not describing the determinisms or semantics of when a transition can fire and who can fire it. We’ll do that in the next step. This just captures the UTXO firing model using the Petri Net.

# “Classical” Petri Net Firing Rules

This is just a more detailed definition. We have `m`, `m` is the marking. `t^-` is the number of Tokens from a given Place that the Transition is required to fire. We have three states here. Obviously in this case the Transition cannot fire because it has insufficient Tokens in its pre-Place. Now it can fire. In that sense it is engaged. Now after it is actually fired it consumes the Tokens, in other words the unspent outputs and it creates an unspent output but it can no longer fire. That is the firing dynamic of Petri Nets.

# Definition: Trace-Net Markings

So we add markings, we add state on top of it. I define that right here. For every Input Arc, an Input Arc pointing from a Place to a Transition. You can think of that as an input of a transaction. We overlay that with a couple of things. We have `h_older`, we have `h_after`. These are basically time counters. For every input I have a `h_older` time counter and that is like the age of the confirmed output. Once this Place becomes populated this counter begins to count. I also have an earliest firing time. The earliest firing time is implied by the output script. If I have a timelock here the earliest firing time is not zero. It is going to be the timelock amount. If I have a nLockTime, that’s the `h_after` my earliest firing time is going to be that nLockTime value. In the absence of timelocks we set the earliest firing time to zero. That is how these time counters work. Once the counters… firing time, this releases the Input Arc. It releases the input that it is modeling. We also have a `w_actor` witness marking and that captures which actor can fire the transition. In Bitcoin a contract doesn’t execute itself. One of the parties executes the contract onchain.

# Definition: Witness Marking

This is just a more convoluted way of defining how that evaluation is made. The witness marking for the transition can have the following values: internal, external, internal and external or nothing. The value it returns is the actor that is currently capable of producing a valid witness for transition t. The value of the witness marking changes as we fire offchain transitions. As we exchange keys and we exchange preimages the actors that can produce a valid one changes. That is the state that is captured here.

# Example: On-Chain Transition Firing

Here is an example. We have our Input Arc markings, we have the `h_older`, `h_after`. We have the earliest firing times and we have the witness marking here. We have the following Script lock for this output, we have an Internal public key and an External public key and we have a timelock, a 10 block delay timelock. At the beginning state there is no actor who can fire the transition. We have the prepopulated Places, we have the UTXO that is available but because it is a multisig output no single actor can fire the Transition. The first Transition that we model here is the sharing of the signature by the Internal Actor. The Internal Actor shares the signature with the counterparty. Once that occurs we have the following state. In this state the witness marking returns the External Actor meaning that the External Actor is the one who can produce a valid witness. But we still have the problem of the timelock. Currently the output `h` counter is at 6 but the earliest firing time implied by the timelock is at 10. It can’t fire. Let’s say we fire a time delay before. That timelock then releases in this marking and t can fire. t fires and produces these two outputs. This is one possible Transition trace for this contract. I illustrate it just to show how the state of the contract changes with each of these Transitions. The goal of this at the end is to exhaustively produce the entire possible state space and then determine or identify the contract execution traces that we consider safe or safe for executing. That means at the end of it I want to be able to know what is the sequence of actions or events that are safe for me to execute which includes the sharing of data or sharing of signatures or broadcast of transactions.

# Example: Trace-Net Model Generation (Atomic Swap)

How do I build a model like that? I have an example of an atomic swap. I think all you guys know how an atomic swap works. We have two transactions. These are just transaction templates at the beginning, they are not signed. Both transactions are funded by counterparties, the Internal Actor and the External Actor. In an atomic swap there are two satisfaction paths that are spendable. There is the one where we do the swap where a preimage is revealed onchain and there is a back out Transition or timeout if the counterparty doesn’t participate. I want to take these two contract templates. I want to be able to automatically model the different state transitions that can occur. This is where Miniscript is very helpful because with Miniscript I know exactly what the satisfaction paths are for every output. There is an interesting thing that we can observe namely for every satisfaction path that is single signer, meaning that it only requires a signature from one actor, that implies that the spending Transition will send it to a destination controlled by that actor. Because it is the signature that controls the destination. So if there is only one pubkey here, then the Transition that spends it along this satisfaction path will implicitly send it to a destination controlled by the Internal Actor and vice versa by the External Actor. The same here. We have this proposed template transaction but because this is a single pubkey satisfaction path there is an implied sweep transaction here as well. We have one sweep transaction here. We have one single signer transaction here with a timelock. And we have a third one here. The destinations of all these implied transactions are known.

From these two transactions we can build our entire skeleton. There is a sweep transaction here that sends to an internal satisfaction path or internal address. There are the two possible single signer transactions here. That’s the skeleton we can now work with. The goal is to take unsigned transaction templates which represent a contract from a contracting protocol and then build out the model with which we then explore the state space. We have defined the different types of transitions that can occur: the exchange of data, time or the broadcast of transactions.

Q - Every possible outcome of a contract?

A - Exactly. Safe or not safe. We first build the entire state space.

# Example: Trace-Net Contract Execution (1)

Here is an example of a possible trace. This is the sequence of transitions. We have the funding transition from the Internal Actor. The External Actor then funds. The Internal Actor then swaps coins thereby revealing the preimage. Then the External Actor swaps with that preimage. I am going to walk you through it and you can check how the state changes. In this case the Internal Actor has funded so you can see the output has moved here. The External Actor can decide to do a couple of things. In this case the External Actor also funds the contract. You can note here currently we are at block height 100 in this example. This is the age of the output, 6 confirmations, but because there is no timelock the earliest fire time is at zero. The Input Arc transitions have released all the Input Arcs. Now the External Actor funds the other contract and the swap now occurs. When the Internal Actor performs the swap transaction the state of the witness marking for this guy changes to External. Once the swap transaction is executed here the hash preimage is released and the External Actor is now able to produce the witness for this guy here which includes the preimage of the same hashlock. 

# Example: Trace-Net Contract Execution (2)

This is another possible trace. We have the Internal Actor that just sweeps. The Internal Actor can move the output to another one that it controls. Subsequently so does the other actor. That is also a possible trace. Note that this is also safe because I get the same funds back so to speak. If my signing policy is an implied balance then this trace is entirely safe. I haven’t lost any funds. I haven’t performed the swap that I wanted to but if the signing policy is balanced then this works as well. 

# Example: Trace-Net Execution (3)

Finally the Abort trace which is also safe in that sense. We have the funding by the Internal Actor. We then have the sweep by the External Actor. The External Actor decides to sweep away. That output is no longer available. Now I have the timeout. Since no other transaction can fire the firing rule goes “If there is a transaction that can fire but only after delay we fire the delay.” The 10 delay is fired. The Input Arc marking goes to 10 so this is released and this Abort transaction can be performed by the Internal Actor.

# Example: Trace-Net State Space Generation

This is a partial representation of the state space by the contract we are using in this example. It starts out at `Z_0`. That’s before the contract has been funded. Here are several examples of possible state traces. We can have a look at what the outcomes are. This outcome where the Internal Actor reveals the hash preimage at the very beginning, that sounds like a bad idea. That’s a trace we can reconstruct. We can determine what the outcome is. It is bad for the Internal Actor because in this case the output is swept by the counterparty. There are traces which are safe. The basic idea is that once you have constructed an entire possible state space, all possible sequences of transitions: the sharing of data, the broadcast of onchain transactions, time delays, you can then determine whether there is a trace that is safe. We can define that in the next slide.

# Definition: Contract Safety

Q - How do you define safe?

A - I have done a bit of a detour to get to the contract safety part but this hopefully captures the intuition. A contract is safe if my policy is defined as “I want to be able to withdraw an expected amount of funds from this contract and I want to be able to do it unilaterally without the counterparty preventing me from doing so.” That is a policy that you can assign internally. In terms of a trace, ideally every transition I can execute myself internally. These are things we can tolerate. Let’s say I can internally reach a contract state which has some trailing transitions which are only fireable by the External Actor. All states here are safe, that’s fine. I can have situations where there is a race. Where the External Actor races me on a state transition. But if the child state that I reach has a safe trace we can tolerate it so that’s fine. That’s the intuition.

Q - Why do you include the sweeping in the state conditions of the swap? When I was waiting for you I thought the other one that’s proposing the swap can then be sure that it is not going to happen. Otherwise I’m not sure why the sweeping is included in the states of the swap.

A - The question was why do I generate a sweep transition here which is implied? Why is that necessary?

Q - I propose a swap to you and then I can do nothing for example and it will fail eventually. Or I can sweep it and it will fail as well. For you there is not really a difference between them. That’s why I wasn’t sure why the sweep was included in this.

A - The sweep is included for one consistency. My rule that I apply here is that if it is a single signer satisfaction path it always has a single signer spend. My funding output is single signer, it is just one public key. The two satisfaction paths timeout or swap which with the preimage are all single signers. For all these satisfaction paths I want to model a single signer transaction. That’s really why. It is consistency. If it is a single signer who can satisfy the satisfaction path then it is always a possibility that a single signer sweeps from there to a destination that it controls. The same goes for the funding output. Even though I have a proposed template transaction here that sends to this contract here, the time and the swap. If I want to consistently apply a rule the same goes for this output. It could be swept. There may be another way to generate the skeleton but that is a consistent rule that has worked. There may be a way to generate a smaller state space that reflects the same safety properties that we want to look for, that’s possible.

Q - Does the safety assume that you act honestly? In a Lightning like scenario where you only get punished if you are dishonest.

A - It doesn’t assume anything about the counterparty. It assumes that you know what sequences are safe. The contract has to be robust against the counterparty trying to interfere in any way possible. If the counterparty tries to race you on certain states by broadcasting a competing transaction your design has to be robust against that. It has to lead to a state where you can still find a safe path back to home so to speak. You are able to withdraw your funds from that state nonetheless.

# Example: Eltoo Payment Channel

I have a more complex example here. We can expand the notion of contract safety here with this example. If you consider eltoo or SIGHASH_NOINPUT there we have rebindable transactions. In a simple eltoo payment transaction I have all these timeout transitions here. If I timeout this is the balance that is being withdrawn. If I update the state of the payment channel, I add another transition that can spend from all the outputs of the states prior to it. The update of the state model looks like this. That’s my new commitment state and these are the transitions that are possible because it is rebindable. That’s cool but we can consider the following. Now there are so many different safe traces. There are so many different ways I can close this contract. I may introduce the idea that I want to understand how does my contract potentially deteriorate as I update it. What do I mean by deteriorate? I want to figure out is there any way I can define the notion of expected contract execution length? As I update this thing do I potentially need more onchain transactions to close a channel? Is that a quantity we can quantify? I want to propose the following. We can for example say there may be a winning strategy that we define for the External Actor. It is in the External Actor’s interest to try to execute the longest path. For example let’s say the counterparty had the most balance at the beginning of the channel life time. The updates were slowly incrementing. The counterparty may want to execute the longest path because the probability of you missing a timeout is maximized that way. We can relax the requirement of respecting the timelock ordering for example and we could say there is a probability at every state that the timeout is missed. The channel is closed with an old state. That’s the basic idea here.

# Symbolic Safety Evaluation: Eltoo Payment Channel

For eltoo that’s pretty interesting. Here we have the current state after funding. I can either timeout to this state which is an old state or I can transition to this state which is the final one. As I update this contract the following happens. There are additional execution paths that are possible. I can reach the final state either this way or this way. The rebindability of these transactions in SIGHASH_NOINPUT allow me to do that. Likewise there is another path to timing out. In this case I have assigned different probability weights to these paths. Without actually assigning the numeric weights we can see that the update does not change the probability of timing out or reaching the successful final state. We can make this symbolic evaluation for this contract. We can say the quality of these traces don’t deteriorate as I update the contract. That’s pretty cool.

We can also compute the expected length of the contract execution. As I update my eltoo channel the paths that I potentially get are getting longer and longer. I can express that symbolically and it turns out this is actually asymptotic. As I update the channel given that the winning strategy for the counterparty is always the longest trace, the expected onchain transaction length however is asymptotic. That is a contract quality that we can potentially describe or verify for in this model.

# Overview: Trace Net Formalism

Just an overview or conclusion. What does this do? It allows us to have real time contract verification. If you give me a bunch of contract transaction templates which are unsigned, with Miniscript and Trace Net I can build a model and explore the entire state space. I can figure out what are safe pathways for me to withdraw the expected funds. Because I can do that I can also apply a generalized policy like a signing policy. I will only sign this contract if the balance is correct, if the withdraw duration respects a certain bound. I can do this across different contract types. It could be a coinjoin, it could be an eltoo payment channel, it could be HTLCs. It should be generalizable over all these different contracts. That is the basic idea. By being able to do so we can decouple the generation of contract templates from the actual signing and the verification thereof. One example of a potential application is you might have a dedicated hardware wallet or HSM or some kind of key manager application that signs contracts generated by protocol implementations above it. One nice implication is for example today we have wallet implementations for all different types of protocols and the liquidity is caught up in each one. I have to move funds onchain or I have to export or transfer private keys. None of that is optimal. I think it is kind of a first step towards potentially having a universal signer that is compatible across different protocols. There are several open questions. We have the problem of state space. If you have a payment channel that has twenty thousand, thirty thousand states especially in eltoo you can imagine that the state space we explore grows exponentially. That is something that we need to consider. Can we use this state space and the traces that it gives us to generate data for external, generalized watchtowers because they know what paths they have to execute to be able to close your contract that you delegate to them? Finally maybe there is some design space for higher order protocols where the clients no longer negotiate specific templates but they negotiate policy. There is some kind of compiler or solver that generates the actual transactions. These transactions could look different from update to update maybe improving privacy. That could be an interesting design space that this would potentially enable.

# Acknowledgements

Just a couple of acknowledgments. A big thank you to the Miniscript guys for answering all my stupid questions, super helpful. Thank you to Josh Harvey. Josh Harvey is CTO of Lamassu. They do Bitcoin ATMs, really cool. They specified a good part of their UI in Petri-Net language. That’s where the idea of specifying contract language in Petri nets started out with. Professor Alberto Lafuente and Andrea Vandlin from the Technical University of Denmark were great sparring partners in terms of the model checking that we applied to this project. I appreciate it is pretty late, thank you for your time. If there are any questions I’d be happy to try to answer them.

# Q&A

Q - The general idea is that you can model a proposed contract and determine if it is good for you to accept it or not?

A - Right and in what sequence it is safe for me to sign.

Q - Under my own signing policy if all of the outcomes are safe I’ll take it but if one of them is not good for me I can reject the policy?

A - Usually there is always a trace that is bad for me but I know what is good for me and what is not good for me. As long as the External Actor can’t force me into a bad trace or a bad sequence it is a safe contract in that sense. It has to be robust against the actor doing something and the actor withholding something. Those are the trace properties we are looking for.

Q - But not robust against you screwing up?

A - No there is nothing that can save you from that.

Q - Generally you have two parties and they having the same principles of what being safe is and not excludes them to interact in the said contract at some point. Eventually they are going to reach a state where this step is bad for me or the other party will say this step is bad for me.

A - The question was a path that is good for me must be bad for the counterparty. We have two actors in this model, the Internal Actor and the External Actor. The verifying actor can verify for the External Actor as well. He can verify both ways. Those paths that are safe for both the External Actor and the Internal Actor are arguably the one that they should negotiate. If I can find a path that is safe for both the External Actor and the Internal Actor being just the Internal Actor then I’ve found the optimal protocol execution sequence for both parties.

Q - I think the point is that they are not mutually exclusive. A path can be good for me and them.

A - Yes.

Q - Is there a way to take into account miner fees? In the atomic swap example you say you get back the same you put in. But it is minus fees.

A - I haven’t modeled any fees here at all. What Chris is saying is that once I have fees this implies that the ability for a transition to be confirmed or propagated… If the fees are insufficient I can’t conduct this onchain transaction. That’s what Chris is suggesting.

Q - I’m saying that it is a cost. Some of that money goes to miners. It should probably be an extra circle.

A - In terms of cost, yes. Or I associate a lower amount to that circle.

Q - There could be attacks where one party could force another party to spend loads of money on miner fees. Not on atomic swaps but on something more complicated.

Q - Just do CPFP. If you have another output you can always CPFP and the main output is going to be the balance of the contract propagated across a stage of transactions.

Q - Safety wouldn’t normally be defined as fee efficiency. But in certain scenarios where the attacker can force you to lose all your funds because of fees then suddenly safety and fee efficiency become blurred. 

Q - It is not about losing funds because your transaction isn’t confirmed. It is that you had to spend some money just to get your money back.

A - Precisely. This eltoo example is motivated by that. As these traces get super long and the winning strategy of the External Actor forces me along the longest trace you can compute the expected onchain length and you can say “Am I willing to pay the fees to confirm all these or not?” We can have a generalized policy for balance but we can also have one for execution cost. We can apply maximum bounds to that. That’s the general idea.

Q - Is Miniscript strictly necessary to create that diagram? Why can’t you just go through all the different scenarios with Script? Are you using the reasoning of Miniscript?

A - I can’t generate the different satisfaction paths that I need. I have my templates that are generated by the atomic swap protocol implementation which gives me these two templates. I need to be able to parse for the satisfaction paths and what Script locks they contain. In this case single signer, I generate a sweep transaction here and here. Single signer, generate sweep transaction over there. It is a pretty basic rule.

Q - You have a piece of software that parses transaction templates or Miniscript templates?

A - Exactly.

Q - You could I suppose write a parser for a specific type of Script. You would reason about that Script manually but in order to have it automated you’d need Miniscript. To have something general you’d need Miniscript.

A - I guess that would be like a coarser version of Miniscript.

Q - It is the template matching.

Q - If you have everything parsed anyway you could add these constraints of how fee races or how eclipse attacks could be and run some Monte Carlo simulations and go through all of them even the stuff that is more difficult to put in the diagram. You could even run it on regtest and have it do all the fee racing and the weird things that you can’t really reason about.

A - What does a fee race mean? A fee race means that I am being prevented from confirming something?

Q - I’m not sure how that happens in practice. You could have an auction or you could have someone making too many childs.

A - I feel that is something a contract design can’t help with. 

Q - You could make it robust against it. You could say “I can never be in a situation where I must spend right now.” Or at least you could indicate the risks. If you do this and this happens in a high fee environment you might be screwed so don’t do it in a high fee environment. 

A - That’s a really good point. We could for example say “I evaluate for time zero and I evaluate for a future where we have confirmed a hundred extra blocks.” Is the contract still safe then or have certain things timed out? That’s entirely possible. For example in these markings here I capture the notion of chain height. The chain height here is 50 and the earliest fire time is zero. We could do this entire evaluation at 51, 52, 53. 

Q - But also prevailing fee rates.

A - Yes.

Q - Your fee rate race is that the counterparty is a miner. You’re racing against his proof of work.

A - This is something I haven’t done yet but you could also do an evaluation for re-org robustness. You could say “For every transition there is the possibility that the blockchain rewinds two blocks or three blocks.” It could be the case that you revealed the preimage but something has been rolled back. What happens there? You could still model that. It follows the same firing rules.

Q - It is more about timelocks and you should scale your claiming timelocks with the value you are pouring into your channel.

A - Exactly.

Q - With normal Lightning right now you have to commit to the fees early on so there is some risk analysis that you could run there. How high should you put the fee?

A - What about the approach of having some probability associated with fee rate at a given time? I sign fees for all these transitions and now I model the entire thing probabilistically. The probability of this trace happening is much higher because the fee rates are higher versus this one.

Q - I don’t know if you care about probabilities rather than worst case scenarios.

Q - The worst case scenario is it is impossible to ever get your transaction onchain. That is a pretty bad scenario.

A - In this case we have relaxed the requirement of timelocks being fired in order and we are modeling everything probabilistically. There is the probability of a timelocked transition firing before another one because you are not vigilant or you are not watching the chain. Watching the chain is a cost. You can still observe how the expected probability of success or failure evolves as you update the contract, as you add states to the channel.

Q - Do you want to talk about Tamarin Prover or not? 

A - That isn’t related to this. I have been thinking about areas where you could potentially take off the shelf to verify protocols. It is still model checking, the whole approach here is model checking. You take a model, you try to exhaustively build its state space and you exhaustively check the state space for safety properties that you define. In a P2P protocol or messaging protocol there are different states we can have that we negotiate. There are good ones and bad ones. That tells me what are safe actions on my part and whether the protocol design allows for me to take these safe execution traces.