Formal security analysis of registration protocols for interactive systems: a methodology and a case of study
Entity
UAM. Departamento de Ingeniería InformáticaDate
2012-09-07Funded by
This work was supported by the UAM project of Teaching Innovation and the Spanish Government project TIN2010-19607.Subjects
InformáticaNote
A version of this paper is in Arxiv.org: arXiv:1201.1134v2Rights
© 2012 The AuthorsEsta obra está bajo una licencia de Creative Commons Reconocimiento-NoComercial-SinObraDerivada 4.0 Internacional.
Abstract
In this work we present and formally analyze CHAT-SRP (CHAos
based Tickets-Secure Registration Protocol), a protocol to provide inter-
active and collaborative platforms with a cryptographically robust solu-
tion to classical security issues. Namely, we focus on the secrecy and au-
thenticity properties while keeping a high usability. In this sense, users are
forced to blindly trust the system administrators and developers. More-
over, as far as we know, the use of formal methodologies for the verifica-
tion of security properties of communication protocols isn’t yet a common
practice. We propose here a methodology to fill this gap, i.e., to analyse
both the security of the proposed protocol and the pertinence of the un-
derlying premises. In this concern, we propose the definition and formal
evaluation of a protocol for the distribution of digital identities. Once
distributed, these identities can be used to verify integrity and source of
information. We base our security analysis on tools for automatic verifica-
tion of security protocols widely accepted by the scientific community, and
on the principles they are based upon. In addition, it is assumed perfect
cryptographic primitives in order to focus the analysis on the exchange of
protocol messages. The main property of our protocol is the incorpora-
tion of tickets, created using digests of chaos based nonces (numbers used
only once) and users’ personal data. Combined with a multichannel au-
thentication scheme with some previous knowledge, these tickets provide
security during the whole protocol by univocally linking each registering
user with a single request. This way, we prevent impersonation and Man
In The Middle attacks, which are the main security problems in registra-
tion protocols for interactive platforms. As a proof of concept, we also
present the results obtained after testing this protocol with real users, at
our university, in order to measure the usability of the registration system.
Files in this item
Google Scholar:Díaz, Jesús
-
Arroyo, David
-
Rodríguez Ortiz, Francisco Borja
This item appears in the following Collection(s)
Related items
Showing items related by title, author, creator and subject.
-
Surgical treatment for colorectal cancer: Analysis of the influence of an enhanced recovery programme on long-term oncological outcomes-a study protocol for a prospective, multicentre, observational cohort study
Ramirez-Rodriguez, Jose M.; Martinez-Ubieto, Javier; Muñoz-Rodes, Jose L.; Rodriguez-Fraile, Jose R.; Garcia-Erce, Jose A.; Blanco-Gonzalez, Javier; Del Valle-Hernandez, Emilio; Abad-Gurumeta, Alfredo; Centeno-Robles, Eugenia; Martinez-Perez, Carolina; Leon-Arellano, Miguel; Echazarreta-Gallego, Estibaliz; Elia-Guedea, Manuela; Pascual-Bellosta, Ana; Miranda-Tauler, Elena; Manuel-Vazquez, Alba; Balen-Rivera, Enrique; Alvarez-Martinez, David; Perez-Peña, Jose; Abad-Motos, Ane; Redondo-Villahoz, Elisabeth; Biosta-Perez, Elena; Guadalajara Labajo, Héctor; Ripollés-Melchor, Javier; Latre-Saso, Cristina; Cordoba-Diaz De Laspra, Elena; Sanchez-Guillen, Luis; Cabellos-Olivares, Mercedes; Longas-Valien, Javier; Ortega-Lucea, Sonia; Ocon-Breton, Julia; Arroyo-Sebastian, Antonio; García Olmo, Damián
2020-10-27