[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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.


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.


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.