[tlaplus] review request: TLA+ model of Katzenpost/tor dirauth protocol

[David Stainton <dstainton415@xxxxxxxxx>]

Greetings TLA+ enthusiasts. I'm writing to request feedback or suggestions.

I've been practicing my TLA+ for the past week and here's my first

model of a real protocol, the Tor/Katzenpost dirauth protocol, it's a simple non-BFT voting protocol which is used by the directory authority nodes of an anonymous communication networks, to create a consensus document containing a view of the network that clients can use.

https://github.com/katzenpost/formal_specifications/blob/main/dirauth/dirauth.tla

Thus far I'm able to write this theorem:

THEOREM ConsensusFailureWithBadActor ==
    /\ \E n \in Nat:
        /\ Cardinality(dirauth_nodes) = n
        /\ Cardinality(bad_actors) = n-3
    => <>[] (phase = "Failed Consensus")

Next I'm thinking that I should make it model dirauth node outages (when a node doesn't respond) or perhaps flaky unreliable dirauth node behavior.

If I did that then I'd be able to write theorem about how node failures can cause "Failed Consensus" state.

Cheers,

David Stainton

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a8835bde-d375-4273-8474-ca05a6f715cfn%40googlegroups.com.