STRIDE Model Checking
Threat modeling with STRIDE is an intuitve way to find leaks in your security design. It is mainly based on a data flow diagram but added with typical threats for element types. STRIDE therefor stands for:
- Spoofing
- Tampering
- Repudiation
- Information Disclosure
- Denial of Service
- Evelation of Privilege
The STRIDE approach defines 5 types of diagram elements: Actors(red), Processes(blue), Databases(white), Data Flow and
Trus Boundaries (red dotted). Based on the STRIDE/Element Matrix you see where to improve your security design.

| Spoofing | Tampering | Repudiation | Inf. Disc. | DoS | Evel. o. Priv. | |
| Actor | yes | yes | ||||
| Process | yes | yes | yes | yes | yes | yes |
| Data Storage | yes | yes | yes | |||
| Data Flow | yes | yes | yes |
I've written a prolog script that helps you to check your threat model. It checks the syntax and tells you if your nodes or data flow links are illegal. It checks additional semantic constraints; And it tells you wether a node is reading data from an untrusted node.
Further Reading
http://msdn.microsoft.com/msdnmag/issues/06/11/ThreatModeling/default.aspx?loc=de