1 of 43

Proof of Byzantine Fault Tolerance

Mathematics of Hashgraph

2 of 43

Assumptions

More of ⅔ of all members are honest and less than ⅓ are not honest.

3 of 43

Assumptions

More of ⅔ of all members are honest and less than ⅓ are not honest.
The digital signatures and cryptographic hashes are secure.

4 of 43

Assumptions

More of ⅔ of all members are honest and less than ⅓ are not honest.
The digital signatures and cryptographic hashes are secure.
If Alice sends Bob all the events she knows, Bob accepts only those that are valid.

5 of 43

Assumptions

More of ⅔ of all members are honest and less than ⅓ are not honest.
The digital signatures and cryptographic hashes are secure.
If Alice sends Bob all the events she knows, Bob accepts only those that are valid.
If Alice and Bob are honest, and Alice repeatedly tries to send Bob a message, she will eventually succeed.

6 of 43

Definitions

c and d are parents of a
c is a self-parent of a

7 of 43

Definitions

c and d are parents of a
c is a self-parent of a
a has the ancestors a, c, d, e, f, g
a has the self-ancestors a, c, g
b is neither an ancestor nor a self-ancestor of a

8 of 43

Definitions

c and d are parents of a
c is a self-parent of a
a has the ancestors a, c, d, e, f, g
a has the self-ancestors a, c, g
b is neither an ancestor nor a self-ancestor of a
A pair of events (a, a’) is a fork if both have the same creator, but neither is a self-ancestor of the other

9 of 43

Definitions

c and d are parents of a
c is a self-parent of a
a has the ancestors a, c, d, e, f, g
a has the self-ancestors a, c, g
b is neither an ancestor nor a self-ancestor of a
A pair of events (a, a’) is a fork if both have the same creator, but neither is a self-ancestor of the other
d can see e, f, g if these events (and their ancestors) does not include a fork
d cannot see a, b, c

10 of 43

Lemma 1: All members have consistent hashgraphs.

11 of 43

Lemma 1: All members have consistent hashgraphs.

Definition:

Two hashgraphs A and B are consistent if for any event x in A and B, both contain the same set of ancestors for x (with the same edges between those ancestors).

12 of 43

Lemma 1: All members have consistent hashgraphs.

Proof:

x

Hashgraph A

Hashgraph B

13 of 43

Lemma 1: All members have consistent hashgraphs.

Proof:

x

y’

z’

y’’

z’’

Hashgraph A

Hashgraph B

14 of 43

Lemma 1: All members have consistent hashgraphs.

Proof:

x

y

z

Hashgraph A

Hashgraph B

15 of 43

Lemma 2 (Strongly Seeing Lemma)

16 of 43

Lemma 2 (Strongly Seeing Lemma)

Definition:

An event x can strongly see y if

x can see y,
there is a set S of events by more than ⅔ of the members such that

x can see every event in S and
every event in S can see y.

S

17 of 43

Lemma 2 (Strongly Seeing Lemma)

If the pair of events (x, y) is a fork and x is strongly seen by v in hashgraph A, then y will not be strongly seen by any event in any hashgraph B that is consistent with A.

18 of 43

Lemma 2 (Strongly Seeing Lemma)

If the pair of events (x, y) is a fork and x is strongly seen by v in hashgraph A, then y will not be strongly seen by any event in any hashgraph B that is consistent with A.

S

A

B

x

y

v

w

A, B

consistent

19 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Assume, there exists a hashgraph B that is consistent with A, such that

S

A

B

x

y

v

w

20 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Part of the members, created events in SA:

21 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Part of the members, created events in SB:

22 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Part of the members, created events in both:

23 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

At least one honest member created events here!

24 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Let Nhan be that member with events

S

A

B

x

y

v

w

25 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Let Nhan be that member with events
Nhan ist honest, so both events cannot be forks

S

A

B

x

y

v

w

26 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Let Nhan be that member with events
Nhan ist honest, so both events cannot be forks
Without loss of generality let be the self-ancestor of

S

A

B

x

y

v

w

27 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Let Nhan be that member with events
Nhan ist honest, so both events cannot be forks
Without loss of generality let be the self-ancestor of
Lemma 1 Hashgraphs A and B are consistent

S

A

B

x

y

v

w

28 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Let Nhan be that member with events
Nhan ist honest, so both events cannot be forks
Without loss of generality let be the self-ancestor of
Lemma 1 Hashgraphs A and B are consistent

S

A

B

x

y

v

w

29 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Let Nhan be that member with events
Nhan ist honest, so both events cannot be forks
Without loss of generality let be the self-ancestor of
Lemma 1 Hashgraphs A and B are consistent

S

A

B

x

y

v

w

30 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Let Nhan be that member with events
Nhan ist honest, so both events cannot be forks
Without loss of generality let be the self-ancestor of
Lemma 1 Hashgraphs A and B are consistent

S

A

B

x

y

v

w

31 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Let Nhan be that member with events
Nhan ist honest, so both events cannot be forks
Without loss of generality let be the self-ancestor of
Lemma 1 Hashgraphs A and B are consistent

S

A

B

x

y

v

w

32 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Let Nhan be that member with events
Nhan ist honest, so both events cannot be forks
Without loss of generality let be the self-ancestor of
Lemma 1 Hashgraphs A and B are consistent

S

A

B

x

y

v

w

33 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Let Nhan be that member with events
Nhan ist honest, so both events cannot be forks
Without loss of generality let be the self-ancestor of
Lemma 1 Hashgraphs A and B are consistent

S

A

B

x

y

v

w

34 of 43

Lemma 2 (Strongly Seeing Lemma)

Proof:

Let Nhan be that member with events
Nhan ist honest, so both events cannot be forks
Without loss of generality let be the self-ancestor of
Lemma 1 Hashgraphs A and B are consistent
Contradiction!

S

A

B

x

y

v

w

35 of 43

Lemma 2 (Strongly Seeing Lemma)

If the pair of events (x, y) is a fork and x is strongly seen by v in hashgraph A, then y will not be strongly seen by any event in any hashgraph B that is consistent with A.

S

A

B

x

y

v

w

A, B

consistent

36 of 43

Summary so far and further implications

At every moment all members will have consistent hashgraphs.
All members will agree on every property of a given event.

37 of 43

Summary so far and further implications

At every moment all members will have consistent hashgraphs.
All members will agree on every property of a given event.

Implications:

The members assign a unique round created number to a given element.
The election votes of a witness are unique.
Theorem: For any single YES/NO question, consensus is achieved eventually with probability 1.
Every round will immutably classify all its witnesses as famous or not famous.

38 of 43

Byzantine Fault Tolerance Theorem

Each event x created by an honest member will eventually be assigned a consensus position in the total order of events, with probability 1.

39 of 43

Demo

The Coq Proof Assistant

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

40 of 43

Any Questions?

41 of 43

Thank you for your attention!

42 of 43

Sources

43 of 43

Contact Details

KrystianGaus@gmail.com

https://www.xing.com/profile/Krystian_Gaus

https://www.linkedin.com/in/krystian-gaus-86aa1b15a/