The Systems Security Modelling and Analysis (SySMA) unit at IMT Lucca deals with the development of languages and techniques for the analysis, evaluation and verification of possibly distributed systems. The SySMA unit goal is to push the use of formal methods as methodological and automatic tools for the development of high-quality, correct software and systems that are secure, fast, usable, reusable, maintainable, and modular. We also study algorithms and systems to protect the security and integrity of computer systems, the information they store, and the people who use them. We make large usage of formal methods as enabling technology also for the security-by-design development model.