Systematic Trojan Detection in Crypto-Systems Using the Model Checker

Formal methods have been introduced as the efficient approach for Trojan detection using the model checking approach. However, systematic property generation for detecting a wide range of Trojans is the main challenge in these methods. In other words, the efficient property generation to pinpoint projected Trojan precisely in targeted hardware has been a bottleneck in this approach. This paper evaluated the feasibility of the systematic property generation methodology for Trojan detection in Cryptosystems by analyzing the vulnerable points of an implemented design respecting Trojans' covered class. The vulnerability analysis reduces the search space of formal methods and considerably improves the scalability of these methods. We have shown in this research that these properties can be generated systematically and prove that the generated properties can be used in conventional model-checking tools to find hard-to-detect Trojans efficiently. Experimental results show that the proposed method reduces Trojan detection time considerably. Also, the memory required to evaluate circuits is possible for several hundreds of clock cycles.