Formal Security Analysis of Registration Protocols for Interactive Systems: A Methodology and a Case of Study
In this paper, the authors present and formally analyze CHAT-SRP (CHAos based Tickets-Secure Registration Protocol), a protocol to provide interactive and collaborative platforms with a cryptographically robust solution to classical security issues. Namely, they focus on the secrecy and authenticity properties while keeping a high usability. Indeed, most interactive platforms currently base their security properties almost exclusively on the correct implementation and configuration of the systems. In this sense, users are forced to blindly trust the system administrators and developers. Moreover, as far as they know, there is a lack of formal methodologies for the verification of security properties for interactive applications.