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) | <NewBlock> | 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 | <receive(x,y)> |
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…