## Blockchain Consensus Algorithm

We have the number of agents that work in parallel that we call validators. Every validator has access to the pull of transactions generated by the participants of blockchain.

Every validator can be fair or to provide the attack. We consider the Double Spending attack. The time is measured by time-slots that is some interval between block creation. We consider that the distribution of validators for block creation is defined from the very beginning and the number of time-slots is equal to the number of validators.

So validator can create a block from the transaction pull in his time slot and receive the blocks in other time slots. When the length of the blockchain part is equal to some fixed value then we declare about finalization and all transaction have to be moved in a ledger but all alternative chains will be removed.

In the process of block sending and receiving the forking of blockchains can occur. It can happen if connection fails or when a malicious validator delays the block sending. The malicious attackers continue the corresponding blockchain that forking shall exist longer time without finalization.

If everything ok then validator creating block put the reference to the last hanging vertex. If forking then fair validator continue the longest blockchain.

We will consider the possibility of attack Double Spending when one of the malicious validators put two transactions with the same ID in two different blocks.

Creation of model

We have N agents that are validators as functional symbol NODE(i).

Environment attributes:

 TIME_SLOT == 1 //time slot number BN == 0 //current block to be created

Agents attributes:

 Forall (1<=i<=N) NODE(i).CHAINS == 1 //current number of chains for i-agent Forall (1<=i<=N) NODE(i).HANG(1) == 0 //initial hanging vertex  (genesis block) for initial blockchain Forall (1<=i<=N) NODE(i).MAX == 1 //the number of maximal length blockchain Forall (1<=i<=N) NODE(i).MIN == 1 //the number of minimal length blockchain Forall (1<=i<=N) NODE(i).LEN(1) = 0 //the length of every blockchain NODE(i).REF_BLOCK(j) //reference of j-block NODE(i).FRAUD //indicator for malicious agent NODE(i).Forking //existence of forking NODE(i).BB //the last created block NODE(i).BC //the last received block

Behavior of validators:

 B0   =( (B(1) || B(2) || B(3) || B(4) || B(5));                             (nextTimeSlot.B0 + !nextTimeSlot.Delta)), // all agents (f.i number of agents is equal 5) work inparallel B(i) = (CreateMode(i);ReceiveMode(i)), // validator can create block or receive it CreateMode(i) = (CreateBlock(i);sendBLock(i)), // creation of blocks and references and sending to other blocks ReceiveMode(i) = receiveBlock(i).checkForking(i).                                                                    (doForking(i) + doHang(i);                                                                            checkMin(i).checkMax(i);                                                                              ReceiveMode (i) + sendBlock(BB(i),i);                                                            ReceiveMode (i) + end(i)), // recevining of blocks in a cycle and sending of delayed blocks (attacks or network problems) CreateBlock(i) =  createBlock(i).                                                                                             (createReferenceFair(i).sendBlock(BN,i) +                                                       createReferenceFraud(i);checkMin(i).checkMax(i)) //block creation, reference creation for malicious and fair validator

Actions:

 Name Precondition Process Postcondition сreateBlock(i) (TIME_SLOT == i) BN = BN + 1; NODE(i).BB = BN+1 createReferenceFair(i) !NODE(i).FRAUD <> NODE(i).REF_BLOCK(BN) = NODE(i).HANG(NODE(i).MAX); NODE(i).HANG(NODE(i).MAX) = BN; NODE(i).LEN(NODE(i).MAX) = NODE(i).LEN(NODE(i).MAX) + 1 createReferenceFraud(i) NODE(i).FRAUD <> NODE(i).REF_BLOCK(BN) = NODE(i).HANG(NODE(i).MIN);            NODE(i).HANG(NODE(i).MIN) = BN; NODE(i).LEN( NODE(i).MIN) = NODE(i).LEN(NODE(i).MIN) + 1 checkMin(i) Forall (1<=j<= NODE(i).CHAINS) && (NODE(i).LEN(j) < NODE(i).LEN(NODE(i).MIN)) <> NODE(i).MIN = j checkMax(i) Forall (1<=j<= NODE(i).CHAINS) && (NODE(i).LEN(j) > NODE(i).LEN(NODE(i).MAX)) <> NODE(i).MAX = j sendBlock(i,b) Forall (1<=j<=N && !(j==i)) < NODE(j): send(b, NODE(i).REF_BLOCK(b)> 1 end(i) 1 <> 1 receiveBlock(i) 1 NODE(i).REF_BLOCK(x) = y; NODE(i).BC = x; NODE(i).Forking checkForking(i) Forall (1<=j<= NODE(i).CHAINS && NODE(i).HANG(j) == NODE(i).REF_BLOCK(NODE(i).BC) <> ! NODE(i).Forking doForking(i) NODE(i).Forking <> NODE(i).CHAINS = NODE(i).CHAINS + 1; NODE(i).LEN(NODE(i).CHAINS) = 1; NODE(i).HANG(NODE(i).CHAINS + 1) = NODE(i).BC(i) doHang(i) ! NODE(i).Forking <> NODE(i).LEN(NODE(i).CHAINS) = NODE(i).LEN(NODE(i).CHAINS) + 1; NODE(i).HANG(NODE(i).CHAINS + 1) = NODE(i).BC nextTimeSlot TIME_SLOT <= N <> TIME_SLOT =  TIME_SLOT + 1

TO BE CONTINUE…