Use formal methods to prove security properties

This is to start a conversation. I am hoping to nerd snipe someone who has the relevant knowledge into doing something I don't know how to do.

I think it would be very helpful to have a Formal Model of TUF. A mathematical model of the server and the client so that proofs can be generated of the security properties. I've seen a lot of questions about "if I just skip this step what security properties do I break", to which the answer is often "more than you realize" because this is a hard complicated problem, but is sometimes "just this one thing, if you don't care about it go ahead". It feels like a formal model would allow people to answer those questions on their own.

I have heard of https://p-org.github.io/P/ which allows modeling entities as state machines, which I think would map really well to the descriptions in the current specification. But I don't think it allows for proofs. I have had TLA+ recommended to me for doing proofs, but it has a far more flexible modeling language. I know that there are many other options available.

Start by reviewing the current TUF specification and the P and TLA+ references mentioned in the issue. Define the scope of a formal server and client model, then determine which security properties and skipped-step questions it should prove; done means a usable model with generated proofs.