Formal Procedural Security Modeling and Analysis