TLA+ spec for Katzenpost dirauth protocol

dirauth.tla

NOTE that in order to use this you'll have to tell your TLA+ model checker about the
values of DirAuthNodes and Relays, for example:

DirAuthNodes <- {"n1","n2","n3","n4","n5"}
Relays <- {"r1", "r2", "r3", "r4", "r5"}

------------------------------ MODULE dirauth ------------------------------

EXTENDS Naturals, Sequences, TLC, FiniteSets

CONSTANT DirAuthNodes, k, Relays

VARIABLES consensus, votes, keys, phase, descriptors, threshold, BadActors

vars == <<consensus, votes, keys, phase, descriptors, threshold, BadActors>>

Init ==
    /\ consensus = <<>>
    /\ votes = [n \in DirAuthNodes |-> <<>>]
    /\ keys = [n \in DirAuthNodes |-> "none"]
    /\ descriptors = [n \in DirAuthNodes |-> {}]
    /\ phase = "KeyGeneration"
    /\ threshold = (Cardinality(DirAuthNodes) \div 2) + 1
    /\ BadActors = {}

BecomeBadActor(n) ==
    /\ phase \in {"KeyGeneration", "DescriptorCollection", "DescriptorExchange", "Vote"}
    /\ n \notin BadActors
    /\ BadActors' = BadActors \union {n}
    /\ UNCHANGED <<votes, consensus, keys, descriptors, phase>>

KeyGeneration(n) ==
    /\ phase = "KeyGeneration"
    /\ UNCHANGED <<votes, consensus, descriptors, BadActors>>
    /\ keys' = [keys EXCEPT ![n] = "key"]
    /\ phase' = "DescriptorCollection"

DescriptorCollection(n, m) ==
    /\ phase = "DescriptorCollection"
    /\ keys[n] /= "none"
    /\ m \in Relays
    /\ UNCHANGED <<votes, consensus, keys, BadActors>>
    /\ descriptors' = [descriptors EXCEPT ![n] = @ \union {m}]
    /\ phase' = "DescriptorExchange"

DescriptorExchange(n, m) ==
    /\ phase = "DescriptorExchange"
    /\ keys[n] /= "none"
    /\ keys[m] /= "none"
    /\ m /= n
    /\ UNCHANGED <<votes, consensus, keys, BadActors>>
    /\ descriptors' = [descriptors EXCEPT ![n] = @ \union descriptors[m]]
    /\ phase' = "Vote"

Consensus ==
    /\ phase = "Consensus"
    /\ UNCHANGED <<votes, keys, descriptors>>
    /\ LET Ups == {n \in DirAuthNodes: Len(votes[n]) > 0 /\ votes[n][Len(votes[n])] = "up"}
       IN Cardinality(Ups) >= threshold
    /\ consensus' = Append(consensus, "up")
    /\ phase' = "KeyGeneration"
 
VoteGood(n, m) ==
    /\ phase = "Vote"
    /\ keys[n] /= "none"
    /\ keys[m] /= "none"
    /\ m /= n
    /\ UNCHANGED <<consensus, keys, descriptors>>
    /\ votes' = [votes EXCEPT ![n] = Append(@, "up")]
    /\ IF \A x \in DirAuthNodes : Len(votes'[x]) > 0 \/ votes'[x][Len(votes'[x])] = "no-vote" 
        THEN phase' = "Consensus"
        ELSE UNCHANGED phase 

VoteBad(n, m) ==
    /\ phase = "Vote"
    /\ keys[n] /= "none"
    /\ keys[m] /= "none"
    /\ m /= n
    /\ n \in BadActors
    /\ UNCHANGED <<consensus, keys, descriptors>>
    /\ votes' = [votes EXCEPT ![n] = Append(@, "down")]
    /\ IF \A x \in DirAuthNodes : Len(votes'[x]) > 0 \/ votes'[x][Len(votes'[x])] = "no-vote"
        THEN phase' = "Consensus"
        ELSE UNCHANGED phase

NoVote(n) ==
    /\ phase = "Vote"
    /\ keys[n] /= "none"
    /\ UNCHANGED <<consensus, keys, descriptors>>
    /\ votes' = [votes EXCEPT ![n] = Append(@, "no-vote")]
    /\ IF \A x \in DirAuthNodes : Len(votes'[x]) > 0 \/ votes'[x][Len(votes'[x])] = "no-vote"
        THEN phase' = "Consensus"
        ELSE UNCHANGED phase

Vote(n, m) ==
    /\ VoteGood(n, m)
    /\ VoteBad(n, m)
    /\ NoVote(n)

Next ==
    /\ threshold' = (Cardinality(DirAuthNodes) \div 2) + 1
    /\ \/ \E N \in SUBSET DirAuthNodes : N /= {} /\ \A n \in N : KeyGeneration(n)
       \/ \E N \in SUBSET DirAuthNodes, M \in SUBSET Relays : N /= {} /\ M /= {} /\ \A n \in N, m \in M : DescriptorCollection(n, m)
       \/ \E N \in SUBSET DirAuthNodes : N /= {} /\ \A n, m \in N : DescriptorExchange(n, m)
       \/ \E N \in SUBSET DirAuthNodes : N /= {} /\ \A n, m \in N : Vote(n, m)
       \/ Consensus

PhaseInvariant == phase \in {"KeyGeneration", "DescriptorCollection", "DescriptorExchange", "Vote", "Consensus"}
KeysInvariant == \A n \in DirAuthNodes : keys[n] \in {"none", "key"}
VotesInvariant == \A n \in DirAuthNodes : \A v \in Seq({"up", "down"}) : v \subseteq votes[n]
ConsensusInvariant == \A v \in Seq({"up", "down"}) : v \subseteq consensus
DescriptorsInvariant == \A n \in DirAuthNodes : descriptors[n] \subseteq Relays
    

Spec == Init /\ [][Next]_vars /\ SF_vars(Next)
         /\ PhaseInvariant /\ KeysInvariant /\ VotesInvariant /\ ConsensusInvariant /\ DescriptorsInvariant


=============================================================================