Architecting Security with Paradigm
Suzana Andova, Luuk Groenewegen, Jan Verschuren and Erik de Vink

For large security systems a clear separation of concerns is achieved through
architecting. Particularly the dynamic consistency between the architectural
components should be addressed, in addition to individual component behaviour.
In this paper, relevant dynamic consistency is specified through Paradigm, a
coordination modeling language based on dynamic constraints. As it is argued,
this fits well with security issues. A smaller example introduces the
architectural approach towards implementing security policies. A larger
casestudy illustrates the use of Paradigm in analyzing the FOO voting scheme.
In addition, translating the Paradigm models into process algebra brings model
checking within reach. Security properties of the examples discussed, are
formally verified with the model checker mCRL2.