REBECCA is a tool for the formal verification of masked cryptographic hardware implementations that, given the netlist of a masked hardware circuit, determines if a correct separation between shares is preserved throughout the circuit. - View it on GitHub