A Formal Analysis of the Mimblewimble Cryptocurrency Protocol

Area of Science:

• Computer Science
• Cryptography
• Software Engineering

Background:

• Mimblewimble (MW) is a privacy-focused cryptocurrency technology.
• It offers distinct security and scalability features compared to other protocols.
• Verifying the correctness of its implementations is crucial for trust and adoption.

Purpose of the Study:

• To present and discuss the unique properties of Mimblewimble.
• To outline a model-driven verification approach for certifying MW protocol implementations.
• To analyze the correctness and security properties of MW.

Main Methods:

• Development of an idealized model for verification.
• Precise statement of conditions ensuring security property verification.
• Creation of a Z specification for a consensus protocol.
• Development of a {log} prototype as an executable model.
• Analysis of Grin and Beam MW implementations.

Main Results:

• An idealized model and its verification conditions were proposed.
• A Z specification and an executable {log} prototype were developed.
• The study provides an analysis of current Grin and Beam MW implementations.
• The model-driven approach facilitates protocol behavior analysis without low-level implementation.

Conclusions:

• The proposed model-driven verification approach is key to certifying Mimblewimble protocol implementations.
• The Z specification and executable prototype enable rigorous analysis of consensus protocols.
• The analysis of Grin and Beam implementations provides insights into the current state of MW technology.