Formal Evaluation and Construction of Glitch-resistant Masked Functions

We give an algorithm that checks whether every possible transition is masked. It allows to verify the absence of first-order leakage from a masked netlist. It validates the state-of-the-art masking schemes, such as Threshold Implementation and Domain Oriented Masking, but also proves that more compact netlists with equivalent functions are secure. We leverage this methodology to propose a more compact implementation of AES S-Box.