The Modular Specifications Security Framework
We present the Modular Specifications Security (MoSS) framework, where security specifications are defined with respect to a specific model predicate M. This allows analysis of even complex schemes and protocols, e.g., PKI schemes, under well-defined adversary, communication and synchronization models, in a modular and flexible way, and allows to analyze such schemes in both simplified and realistic models. The framework facilitates reuse of definitions, and, indeed, several of the model predicates and security specifications we define, seem ‘generic’ and reusable in analysis of other practical protocols.