Due to cost and time reasons, hardware development is currently often done using IP of external vendors and outsourcing of fabrication to third parties. This leads to a globalization of the supply chain, which highly increases the risk of inserted Hardware Trojans (HTs). HTs are malicious modifications of hardware to change hardware functionality or to leak secret data. Especially in safety- and security-critical areas like autonomous driving, Hardware Trojans can cause severe consequences and endanger even human lives. For this reason, we present in this work how model checking based formal verification can be used in a systematic way to detect HTs reliably. We are the first additionally using signal connection properties on top of design functionality properties for reliable HT detection and full HT detection coverage. To reduce verification time and strongly increase HT detection coverage, we developed a tool to generate a high number of properties automatically. Additionally, we intend to publish a large set of specification and microarchitecture intent derived properties important for HT detection in processors and show how these properties have to be combined with connection properties for reliable HT detection. We finished our work on identifying a complete property set for detecting each inserted Hardware Trojan for the Program Counter at an arbitrary position in a RISC-V processor. In this paper we present this property set and HT detection properties writing guidelines we identified during this work. Experimental results confirm we get the full proofs needed for reliable Hardware Trojan detection for all properties in below $24$ hours. Our work will result in a guideline for reliable HT detection in processors using formal verification.