Formal Verification of ASCON Cipher using JasperGold

ASCON, a finalist in the CAESAR competition for authenticated encryption, is optimized for resource-constrained environments such as IoT devices. Ensuring its security and correctness is critical for its adoption in these applications. In this work, the hardware design of the ASCON cryptographic algorithm is verified using formal methods in the Cadence JasperGold Formal Property Verification app. The tool is utilized to verify the properties and correctness of the implemented ASCON design. It offers a mathematical approach to confirm that the implementation adheres to its specification without the need for generating input combinations manually, effectively identifying corner cases and vulnerabilities. A comprehensive set of properties and assertions for ASCON 128 and 128a, including functional correctness, control path and data path correctness, and state transitions, is defined for verification in the System Verilog language for both encryption and decryption. The Jasper-Gold FPV tool systematically analyzes these properties across all possible input scenarios. The verification results indicate that the hardware implementation of ASCON satisfies all defined properties, demonstrating its robustness and reliability.