CRYSTAL mainly focuses on assessing the security aspects of Cyber-Physical Systems. In this project, we use Timed Rebeca and model checker Afra to specify and verify the behavior of CPS components against CPS-related attacks. We analyze architecture of CPS design to recognize where the potential attacks can successfully lead the system to security violation.
A model of attack is proposed for both attacks on CPS communication and components. Also, we utilize the STRIDE model (a model of threats is used at Microsoft for identifying computer security threats) as a reference for classifying the attacks. Currently, we are extending our work to analyze mitigation strategies against CPS-related attacks and also verifying security of the system using run-time verification.