Using SPIN and eclipse for optimized high-level modeling and analysis of computer network attack models

摘要: Advanced attack sequences combine different kinds of steps (e.g. attacker, protocol, and administration steps) on multiple networked systems. We propose a SPIN based approach for formal modeling analysis such scenarios. Our is especially suited scenarios were protocol network level aspects matter simultaneously. Typical not yet considered variants can be automatically found. The development scenario models supported by framework the use high-level process specification language cTLA. A compiler translates cTLA to Promela. This allows powerful model-checking tool employed analysis. Through integration into Eclipse platform both model are facilitated.