Create a gist now

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment