Consensus protocol security analysis using an algebraic virtual machine

Abstract

The paper presents the behavior algebra formal methods for application within the consensus protocol security analysis domain in the scope of the program system AVM (Algebraic Virtual Machine). It was developed on the basis of behavior algebra and the theory of interaction of agents and environments. AVM allows the use of different methods for analysis of system properties, detection of the behavior given as algebraic patterns, and symbolic modeling of system behavior. The simplified version of Proof of Stake protocol is considered as the example of application of the algebraic approach for resolving the problem of checking resistance to attacks and reachability of undesirable properties. The study presents formalization of the protocol and its properties as behavior algebra equations. Methods of property reachability and analysis in the scope of behavior algebra such as symbolic modelling and algebraic matching are considered. The works are in progress and the study demonstrates the first applications of the approach.