bb_orchestrator_machine

machine bb_orchestrator_machine sees bb_orchestrator_context

variables config config_signatures shares shares_signatures public_key public_key_signatures
			vote_started votes mixes mixes_signatures decryptions decryptions_signatures
			plaintext plaintext_signatures process_end

invariants
  @inv0 config ∈ BOOL @inv1 config_signatures ∈ ℙ(1 ‥ privacy_level)
  @inv2 shares ∈ ℙ(1 ‥ privacy_level) @inv3 shares_signatures ∈ ℙ(1 ‥ privacy_level)
  @inv4 public_key ∈ BOOL @inv5 public_key_signatures ∈ ℙ(1 ‥ privacy_level)
  @inv6 vote_started ∈ BOOL @inv7 votes ∈ BOOL
  @inv8 mixes ∈ ℙ(1 ‥ privacy_level) @inv9 mixes_signatures ∈ ℙ(1 ‥ privacy_level)
  @inv10 decryptions ∈ ℙ(1 ‥ privacy_level) @inv11 decryptions_signatures ∈ ℙ(1 ‥ privacy_level)
  @inv12 plaintext ∈ BOOL @inv13 plaintext_signatures ∈ ℙ(1 ‥ privacy_level)
  @inv14 process_end ∈ BOOL

  // prover hand holding

  // this should be obvious as the biggest set in POW(A) is |A|
  @set_sizes card(config_signatures) ≤ privacy_level ∧ card(shares) ≤ privacy_level ∧
  	 card(shares_signatures) ≤ privacy_level ∧ card(public_key_signatures) ≤ privacy_level ∧
  	 card(mixes) ≤ privacy_level ∧ card(mixes_signatures) ≤ privacy_level ∧
  	 card(decryptions) ≤ privacy_level ∧ card(decryptions_signatures) ≤ privacy_level ∧
  	 card(plaintext_signatures) ≤ privacy_level

  // should also be obvious as negating the < leaves only the = possibility
  theorem @t1 ¬(card(config_signatures)<privacy_level) ⇒  card(config_signatures)=privacy_level
  theorem @t2 ¬(card(shares)<privacy_level) ⇒ (card(shares)=privacy_level)
  theorem @t3 ¬(card(shares_signatures)<privacy_level) ⇒ (card(shares_signatures)=privacy_level)
  theorem @t4 ¬(card(mixes)<privacy_level) ⇒ (card(mixes)=privacy_level)
  theorem @t5 ¬(card(mixes_signatures)<privacy_level) ⇒  (card(mixes_signatures)=privacy_level)
  theorem @t6 ¬(card(decryptions)<privacy_level) ⇒ (card(decryptions)=privacy_level)
  theorem @t7 ¬(card(decryptions_signatures)<privacy_level) ⇒ (card(decryptions_signatures)=privacy_level)
  theorem @t8 ¬(card(plaintext_signatures)<privacy_level) ⇒  (card(plaintext_signatures)=privacy_level)

  // sanity checks, forward (do not remove as some theorems proofs will fail)
  @step1 config=FALSE ⇒  card(config_signatures) = 0
  @step2 card(config_signatures) < privacy_level ⇒  card(shares) = 0
  @step3 card(shares) < privacy_level ⇒  card(shares_signatures) = 0
  @step4 card(shares_signatures) < privacy_level ⇒ public_key = FALSE
  @step5 public_key = FALSE ⇒ vote_started = FALSE
  @step6 vote_started = FALSE ⇒ votes = FALSE
  @step7 votes = FALSE ⇒  card(mixes) = 0
  @step8 card(mixes) < privacy_level ⇒  card(mixes_signatures) = 0
  @step9 card(mixes_signatures) < privacy_level ⇒  card(decryptions) = 0
  @step10 card(decryptions) < privacy_level ⇒  card(decryptions_signatures) = 0
  @step11 card(decryptions_signatures) < privacy_level ⇒  plaintext = FALSE
  @step12 plaintext = FALSE ⇒  card(plaintext_signatures) = 0
  @step13 card(plaintext_signatures) < privacy_level ⇒  process_end = FALSE

  // sanity checks, backward (do not remove as some theorems proofs will fail)
  @step14 process_end = TRUE ⇒ card(plaintext_signatures) = privacy_level
  @step15 card(plaintext_signatures) = privacy_level ⇒ plaintext = TRUE
  @step16 plaintext = TRUE ⇒ card(decryptions_signatures) = privacy_level
  @step17 card(decryptions_signatures) = privacy_level ⇒  card(decryptions) = privacy_level
  @step18 card(decryptions) = privacy_level ⇒ card(mixes_signatures) = privacy_level
  @step19 card(mixes_signatures) = privacy_level ⇒ card(mixes) = privacy_level
  @step20 card(mixes) = privacy_level ⇒  votes = TRUE
  @step21 votes = TRUE ⇒  vote_started = TRUE
  @step22 vote_started = TRUE ⇒  public_key = TRUE
  @step23 public_key = TRUE ⇒ card(shares_signatures) = privacy_level
  @step24 card(shares_signatures) = privacy_level ⇒  card(shares) = privacy_level
  @step25 card(shares) = privacy_level ⇒ card(config_signatures) = privacy_level
  @step26 card(config_signatures) = privacy_level ⇒ config = TRUE

  // example theorem: the vote cannot start unless the public key exists
  theorem @example public_key = FALSE ⇒ vote_started = FALSE
  // example theorem: decryptions cannot start unless the mixes are finished
  theorem @example2 card(mixes) < privacy_level ⇒  card(decryptions) = 0
  // example theorem: the plaintext cannot exist if the mixes havent been signed
  theorem @example3 card(mixes_signatures) < privacy_level ⇒  plaintext = FALSE

  // for some reason we need to help the prover up to this point
  // we are negating the below theorem clause by clause
  theorem @t9 ¬(config=FALSE) ∧
  	¬(config=TRUE ∧ card(config_signatures)<privacy_level) ∧
  	¬(card(config_signatures) = privacy_level ∧ card(shares) < privacy_level) ∧
  	¬(card(shares) = privacy_level ∧ card(shares_signatures) < privacy_level) ∧
  	¬(card(shares_signatures) = privacy_level ∧  public_key=FALSE) ∧
  	¬(public_key =TRUE ∧ vote_started = FALSE) ∧
  	¬(vote_started = TRUE ∧ votes = FALSE)
  	⇒  votes = TRUE

  // prove that the protocol is deadlock free besides the end state
  theorem @termination (config = FALSE) ∨  (config = TRUE ∧ card(config_signatures) < privacy_level) ∨
     (card(config_signatures) = privacy_level ∧ card(shares) < privacy_level) ∨
     (card(shares) = privacy_level ∧ card(shares_signatures) < privacy_level) ∨
     (card(shares_signatures) = privacy_level ∧  public_key = FALSE) ∨
     (public_key = TRUE ∧ vote_started = FALSE) ∨  (vote_started = TRUE ∧ votes = FALSE) ∨
     (votes = TRUE ∧ card(mixes) < privacy_level) ∨
     (card(mixes) = privacy_level ∧ card(mixes_signatures) < privacy_level) ∨
     (card(mixes_signatures) = privacy_level ∧ card(decryptions) < privacy_level) ∨
     (card(decryptions) = privacy_level ∧ card(decryptions_signatures) < privacy_level) ∨
     (card(decryptions_signatures) = privacy_level ∧  plaintext = FALSE) ∨
	 (plaintext = TRUE ∧ card(plaintext_signatures) < privacy_level) ∨
	 (card(plaintext_signatures) = privacy_level ∧  process_end = FALSE) ∨
	 process_end = TRUE

  // TODO prove the process will terminate

events
  event INITIALISATION
    then
      @act0 config ≔ FALSE @act1 config_signatures ≔ ∅
      @act2 shares ≔ ∅  @act3 shares_signatures ≔ ∅
      @act4 public_key ≔ FALSE @act5 public_key_signatures ≔ ∅
      @act6 vote_started ≔ FALSE @act7 votes ≔ FALSE
      @act8 mixes ≔ ∅  @act9 mixes_signatures ≔ ∅
      @act10 decryptions ≔ ∅  @act11 decryptions_signatures ≔ ∅
      @act12 plaintext ≔ FALSE @act13 plaintext_signatures ≔ ∅
      @act14 process_end ≔ FALSE
  end

  event admin_start
  	where
  	  @grd1 config = FALSE
  	then
  	  @start config ≔ TRUE
  end

   event trustee_sign_config
  	any
  	  trustee
  	where
  	  @trustee trustee ∈  1 ‥ privacy_level ∧ trustee ∉ config_signatures
  	  @grd1 config = TRUE ∧ card(config_signatures) < privacy_level
  	then
  	  @go config_signatures ≔ config_signatures ∪ {trustee}
  end

  event trustee_create_share
  	any
  	  trustee
  	where
  	  @trustee trustee ∈  1 ‥ privacy_level ∧ trustee ∉ shares
  	  @grd1  card(config_signatures) = privacy_level ∧ card(shares) < privacy_level
  	then
  	  @go shares ≔ shares ∪ {trustee}
  end

   event trustee_sign_shares
  	any
  	  trustee
  	where
  	  @trustee trustee ∈  1 ‥ privacy_level ∧ trustee ∉ shares_signatures
  	  @grd1 card(shares) = privacy_level ∧ card(shares_signatures) < privacy_level
  	then
  	  @go shares_signatures ≔ shares_signatures ∪ {trustee}
  end

  event trustee_combine_shares
  	any
  	  trustee
  	where
  	  @trustee trustee = 1
  	  @grd1 card(shares_signatures) = privacy_level ∧  public_key = FALSE
  	then
  	  @go public_key ≔ TRUE
  end

  event admin_start_vote
  	where
  	  @grd1 public_key = TRUE ∧ vote_started = FALSE
  	then
  	  @start vote_started ≔ TRUE
  end

  event admin_end_vote
  	where
  	  @grd1 vote_started = TRUE ∧ votes = FALSE
  	then
  	  @start votes ≔ TRUE
  end

  event trustee_create_mix
  	any
  	  trustee
  	where
  	  @trustee trustee ∈  1 ‥ privacy_level ∧ trustee ∉ mixes
  	  @grd1  votes = TRUE ∧ card(mixes) < privacy_level
  	then
  	  @go mixes ≔ mixes ∪ {trustee}
  end

  event trustee_sign_mixes
  	any
  	  trustee
  	where
  	  @trustee trustee ∈  1 ‥ privacy_level ∧ trustee ∉ mixes_signatures
  	  @grd1 card(mixes) = privacy_level ∧ card(mixes_signatures) < privacy_level
  	then
  	  @go mixes_signatures ≔ mixes_signatures ∪ {trustee}
  end

  event trustee_create_decryption
  	any
  	  trustee
  	where
  	  @trustee trustee ∈  1 ‥ privacy_level ∧ trustee ∉ decryptions
  	  @grd1 card(mixes_signatures) = privacy_level ∧ card(decryptions) < privacy_level
  	then
  	  @go decryptions ≔ decryptions ∪ {trustee}
  end

  event trustee_sign_decryptions
  	any
  	  trustee
  	where
  	  @trustee trustee ∈  1 ‥ privacy_level ∧ trustee ∉ decryptions_signatures
  	  @grd1 card(decryptions) = privacy_level ∧ card(decryptions_signatures) < privacy_level
  	then
  	  @go decryptions_signatures ≔ decryptions_signatures ∪ {trustee}
  end

  event trustee_combine_decryptions
  	any
  	  trustee
  	where
  	  @trustee trustee = 1
  	  @grd1 card(decryptions_signatures) = privacy_level ∧  plaintext = FALSE
  	then
  	  @go plaintext ≔ TRUE
  end

  event trustee_sign_plaintext
  	any
  	  trustee
  	where
  	  @trustee trustee ∈  1 ‥ privacy_level ∧ trustee ∉ plaintext_signatures
  	  @grd1 plaintext = TRUE ∧ card(plaintext_signatures) < privacy_level
  	then
  	  @go plaintext_signatures ≔ plaintext_signatures∪ {trustee}
  end

  event admin_end
  	where
  	  @grd1 card(plaintext_signatures) = privacy_level ∧  process_end = FALSE
  	then
  	  @go process_end ≔ TRUE
  end

end