Abstract
Detecting vulnerabilities, including hardware Trojans, in third-party intellectual property (3PIP) is a rising security challenge for modern day System-on-Chips (SoCs). This work proposes a new approach for detecting security vulnerabilities in a SoC containing 3PIP by breaking complex security flows into fine-grained security properties which are subject to formal verification.