Security has become an essential and critical nonfunctional requirement of modern software systems, especially cyber physical systems. Security patterns aim at capturing security expertise in the worked solutions to recurring security design problems. This paper presents an approach to formally model and analyze six security patterns to detect potential incompleteness, inconsistency, and ambiguity in the textual descriptions; and to prevent their incorrect implementation. These patterns are modeled using high level Petri nets in our tool environment PIPE+. Simulation is used to analyze various security relevant properties. The validated formal models of individual security patterns serve as the building blocks for system design involving the composition of multiple security patterns.
