Paradigm protocol verification The coordination modeling language Paradigm [1] considers distributed sysems of interacting component. Paradigm distinguishes between the component level, governed by the local transitions of a component, and the interaction level, governed by so-called consistency rules. Recently, Paradigm has been extended to deal with data regarding the modeling of interaction among components. In [2] the translation of Paradigm, without data, to the process language of the mCRL2 toolset is described. Goal of the project is to adapt and implement the translation. Validation of the approach is aimed to be done by the analysis of a number of security protocols, like the Needham-Schroeder protocol [3] or the FOO voting scheme [4]. [1] L. Groenewegen and E.P. de Vink, Operational semantics for Coordination in Paradigm, Proc. Coordination 2002, York, April 2002, F. Arbab and C. Talcott (eds.), LNCS 2315, p191-206. [2] S. Andova, L.P.J. Groenewegen and E.P. de Vink, Dynamic Adaptation with Distributed Control in Paradigm, Science of Computer Programming 94, p333-361. [3] G. Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Software-Concepts and Tools 17, 1996, pages 93-102. [4] S. Mauw, J. Verschuren and E.P. de Vink, Data Anonymity in the FOO Voting Scheme, Proc. VODCA 2006, Bertinoro, Italy, M. ter Beek and F. Gadducci (eds.), ENTCS 168, 2007, pages 5-28.