@article {JavierLopez2005b, title = {Security Protocols Analysis: A SDL-based Approach}, journal = {Computer Standards \& Interfaces}, volume = {27}, number = {3}, year = {2005}, pages = {489-499}, publisher = {Elsevier}, abstract = {

Organizations need to develop formally analyzed systems in order to achieve well-known formal method benefits. In order to study the security of communication systems, we have developed a methodology for the application of the formal analysis techniques, commonly used in communication protocols, to the analysis of cryptographic protocols. In particular, we have extended the design and analysis phases with security properties. Our proposal uses a specification notation based on one of the most used standard requirement languages HMSC/MSC, which can be automatically translated into a generic SDL specification. The SDL system obtained can then be used for the analysis of the addressed security properties, by using an observer process schema. Besides our main goal to provide a notation for describing the formal specification of security systems, our proposal also brings additional benefits, such as the study of the possible attacks to the system, and the possibility of re-using the specifications produced to describe and analyse more complex systems.

}, issn = {0920-5489}, author = {Javier Lopez and Juan J. Ortega and Jose M. Troya} } @inproceedings {1735, title = {Especificaci{\'o}n formal y verificaci{\'o}n de requisitos de Seguridad}, booktitle = {VIII Reuni{\'o}n Espa{\~n}ola sobre Criptolog{\'\i}a y Seguridad de la Informaci{\'o}n (VIII RECSI)}, year = {2004}, month = {Sep 2004}, pages = {225-235}, address = {Madrid (Spain)}, isbn = {84-7978-650-7}, author = {Isaac Agudo and Javier Lopez and Juan J. Ortega} } @article {AntonioMana2004, title = {A Framework for Secure Execution of Software}, journal = {International Journal of Information Security (IJIS)}, volume = {3}, number = {2}, year = {2004}, pages = {99-112}, publisher = {Springer}, abstract = {

The protection of software applications is one of the most important problems to solve in information security because it has a crucial effect on other security issues.We can find in the literature many research initiatives that have tried to solve this problem, many of them based on the use of tamperproof hardware tokens. This type of solutions depends on two basic premises: (i) to increase the physical security by using tamperproof devices, and (ii) to increase the complexity of the analysis of the software. The first premise is reasonable. The second one is certainly related to the first one. In fact, its main goal is that the pirate user can not modify the software to bypass an operation that is crucial: checking the presence of the token. However, the experience shows that the second premise is not realistic because the analysis of the executable code is always possible. Moreover, the techniques used to obstruct the analysis process are not enough to discourage an attacker with average resources.

In this paper, we review the most relevant works related to software protection, present a taxonomy of those works and, most important, we introduce a new and robust software protection scheme. This solution, called SmartProt, is based on the use of smart cards and cryptographic techniques, and its security relies only on the first of previous premises; that is, Smartprot has been designed to avoid attacks based on code analysis and software modification. The entire system is described following a lifecycle approach, explaining in detail the card setup, production, authorization, and execution phases. We also present some interesting applications of Smart- Prot as well as the protocols developed to manage licenses. Finally, we provide an analysis of its implementation details.

}, issn = {1615-5262}, author = {Antonio Mana and Javier Lopez and Juan J. Ortega and Ernesto Pimentel and Jose M. Troya} } @article {JavierLopez2004b, title = {PKI Design Based on the Use of On-line Certification Authorities}, journal = {International Journal of Information Security (IJIS)}, volume = {2}, number = {2}, year = {2004}, pages = {91-102}, publisher = {Springer}, abstract = {

Public-Key Infrastructures (PKIs) are considered the basis of the protocols and tools needed to guarantee the security demanded for new Internet applications like electronic commerce, government-citizen relationships and digital distribution. This paper introduces a new infrastructure design, Cert{\textquoteright}eM, a key management and certification system that is based on the structure of the electronic mail service and on the principle of near-certification. Cert{\textquoteright}eM provides secure means to identify users and distribute their public-key certificates, enhances the efficiency of revocation procedures, and avoids scalability and synchronization problems. Because we have considered the revocation problem as priority in the design process, and with a big influence in the rest of the PKI components, we have developed an alternative solution to the use of Certificate Revocation Lists (CRLs), which has become one of the strongest points in this new scheme.

}, issn = {1615-5262}, author = {Javier Lopez and Antonio Mana and Jose A. Montenegro and Juan J. Ortega} } @inproceedings {JavierLopez2003b, title = {Applying SDL to Formal Analysis of Security Systems}, booktitle = {11th International SDL Forum (SDL{\textquoteright}03)}, series = {LNCS}, volume = {2708}, year = {2003}, month = {July}, pages = {300-317}, publisher = {Springer-Verlag}, organization = {Springer-Verlag}, address = {Stuttgart, Germany}, abstract = {

Nowadays, it is widely accepted that critical systems have to be formally analysed in order to achieve well-known formal method benefits. In order to study the security of communication systems, we have developed a methodology for the application of the formal analysis techniques commonly used in communication protocols to the analysis of cryptographic ones. In particular, we have extended the design and analysis phases with security properties. Our proposal uses a specification notation based on MSC, which can be automatically translated into a generic SDL specification. This SDL system can then be used for the analysis of the desired security properties, by using an observer process schema. Apart from our main goal of providing a notation for describing the formal specification of security systems, our proposal also brings additional benefits, such as the study of the possible attacks to the system, and the possibility of re-using the specifications produced to describe and analyse more complex systems.

}, author = {Javier Lopez and Juan J. Ortega and Jose M. Troya} } @inproceedings {javierlopez2003, title = {High-level Specification of Security Systems}, booktitle = {IEEE Globecom 2003 - Communications Security Track}, year = {2003}, month = {December}, pages = {1506-1510}, publisher = {IEEE Press}, organization = {IEEE Press}, address = {San Francisco}, abstract = {

In order to study the security systems, we have developed a methodology for the application to the analysis of cryptographic protocols of the formal analysis techniques commonly used in communication protocols. In particular, we have extended the design and analysis phases with security properties. Our proposal uses a specification notation based on HMSC/MSC, which can be automatically translated into a generic SDL specification.

}, isbn = {0-7803-7974-8}, author = {Javier Lopez and Juan J. Ortega and Jose M. Troya and Jose L. Vivas} } @inproceedings {javierlopez2003a, title = {How to Specify Security Services: A Practical Approach}, booktitle = {7th IFIP Conference on Multimedia and Communications Security (CMS{\textquoteright}03)}, series = {LNCS}, volume = {2828}, year = {2003}, month = {October}, pages = {158-171}, publisher = {Springer-Verlag}, organization = {Springer-Verlag}, address = {Torino, Italy}, abstract = {

Security services are essential for ensuring secure communications. Typically no consideration is given to security requirements during the initial stages of system development. Security is only added latter as an afterthought in function of other factors such as the environment into which the system is to be inserted, legal requirements, and other kinds of constraints. In this work we introduce a methodology for the specification of security requirements intended to assist developers in the design, analysis, and implementation phases of protocol development. The methodology consists of an extension of the ITU-T standard requirements language MSC and HMSC, called SRSL, defined as a high level language for the specification of security protocols. In order to illustrate it and evaluate its power, we apply the new methodology to a real world example, the integration of an electronic notary system into a web-based multi-users service platform.

}, isbn = {3-540-20185-8}, author = {Javier Lopez and Juan J. Ortega and Jose M. Troya and Jose L. Vivas} } @article {JavierLopez2003c, title = {Integrating PMI Services in CORBA Applications}, journal = {Computer Standards \& Interfaces}, volume = {25}, number = {4}, year = {2003}, pages = {391-409}, abstract = {

Application-level access control is an important requirement in many distributed environments. For instance, in new scenarios such as e-commerce, access to resources by previously unknown users is an essential problem to be solved. The integration of Privilege Management Infrastructure (PMI) services in the access control system represents a scalable way to solve this problem. Within the CORBA standards, the Resource Access Decision (RAD) facility is a mechanism used by security-aware applications to obtain authorization decisions and to manage access decision policies. This paper presents PMI-RAD, an approach to integrate the services of an external PMI into CORBA applications using the RAD facility. In particular, the integration of the external PMI in the access control system is based on the semantic description of the PMI services. Our RAD implementation requests and verifies attribute certificates from the PMI in a transparent way for CORBA objects.

}, issn = {0920-5489}, author = {Javier Lopez and Antonio Mana and Juan J. Ortega and Jose M. Troya and Mariemma I. Yague} } @inproceedings {JavierLopez2002f, title = {Designing Software Tools for the Use of Secure Electronic Forms}, booktitle = {3rd ACIS Int. Conf. on Software Engineering, Artificial Intelligence Networking and Parallel/Distributed Computing (SNPD{\textquoteright}02)}, year = {2002}, month = {Junio}, pages = {157-163}, address = {Madrid, Spain)}, abstract = {

Interaction of organizations and their clients by using the Internet can produce meaningful benefits in the accessibility, efficiency and availability of documents, regardless of time and location. However, some types of problems hinder a higher degree of communication. This paper presents some of the results of a Research Project that focuses on the influence of typical open networks risks in electronic interactions and on the need of creating software tools to manage electronic versions of the paper-based forms, as this is the traditional way of interaction through the Web.

}, author = {Javier Lopez and Antonio Mana and Jose A. Montenegro and Juan J. Ortega and Jose M. Troya} } @inproceedings {JavierLopez2002h, title = {Observaciones sobre las t{\'e}cnicas de an{\'a}lisis formal de protocolos de seguridad}, booktitle = {VII Reuni{\'o}n Espa{\~n}ola sobre Criptolog{\'\i}a y Seguridad de la Informaci{\'o}n (VII RECSI)}, year = {2002}, month = {Septiembre}, pages = {471-483}, address = {Oviedo, Espa}, abstract = {

La aplicaci\ón de los m\étodos formales para el dise\ño y an\álisis de sistemas cr\íticos est\á ampliamente aceptada en el desarrollo de estos sistemas. Los protocolos de seguridad abordan el objetivo de garantizar servicios y derechos como el de la confidencialidad de los datos personales o el de garantizar la identidad de acceso a un sistema. Por lo tanto, ya que un protocolo de seguridad es un sistema cr\ítico, es necesario utilizar m\étodosformales para su dise\ño y an\álisis. Debido a las caracter\ísticas especiales que presentan este tipo de protocolos, se deben utilizar m\étodos que no son los tradicionales utilizados para los protocolos de comunicaciones, sino que deben utilizarse otros espec\íficos. En este art\ículo vamos a hacer un estudio de las principales propiedades de seguridad que poseen los protocolos criptogr\áficos y de la manera de aplicar los m\étodos formales en su dise\ño y an\álisis.

}, author = {Javier Lopez and Sonia Matamoros and Juan J. Ortega and Jose M. Troya} } @inproceedings {JavierLopez2002, title = {Protecci{\'o}n de Software basada en Tarjetas Inteligentes}, booktitle = {VII Reuni{\'o}n Espa{\~n}ola sobre Criptolog{\'\i}a y Seguridad de la Informaci{\'o}n (VII RECSI)}, year = {2002}, month = {Septiembre}, pages = {485-497}, address = {Oviedo, Espa}, author = {Javier Lopez and Antonio Mana and Juan J. Ortega and Ernesto Pimentel} } @inproceedings {JavierLopez2002b, title = {Protocol Engineering Applied to Formal Analysis of Security Systems}, booktitle = {International Conference on Infrastructure Security (InfraSec{\textquoteright}02)}, series = {LNCS}, volume = {2437}, year = {2002}, month = {October}, pages = {246-259}, publisher = {Springer-Verlag}, organization = {Springer-Verlag}, address = {Bristol, U.K.}, abstract = {

Every communication system requiring security properties is certainly critical. In order to study the security of communication systems, we have developed a methodology for the application of the formal analysis techniques of communication protocols to the analysis of cryptographic ones. We have extended the design and analysis phases with security properties. Our methodology uses a specification technique based on the HMSC/MSC requirement languages, and translates it into a generic schema for the SDL specification language, which is used for the analysis. Thus, the technique allows the specification of security protocols using a standard formal language and uses Object-Orientation for reusability purposes. The final goal is not only the formal specification of a security system, but to examine the possible attacks, and later use the specification in more complex systems.

}, author = {Javier Lopez and Juan J. Ortega and Jose M. Troya} } @inproceedings {JavierLopez2002g, title = {Towards a Trustful and Flexible Environment for Secure Communications with Public Administrations}, booktitle = {First International Conference on Electronic Government (EGOV{\textquoteright}02)}, series = {LNCS}, volume = {2456}, year = {2002}, month = {September}, pages = {211-214}, publisher = {Springer}, organization = {Springer}, address = {Aix-en-Provence, France)}, abstract = {

Interaction of citizens and private organizations with Public Administrations can produce meaningful benefits in the accessibility, efficiency and availability of documents, regardless of time, location and quantity. Although there are some experiences in the field of e-government there are still some technological and legal difficulties that avoid a higher rate of communications with Public Administrations through Internet, not only from citizens, but also from private companies. We have studied two of the technological problems, the need to work in a trustful environment and the creation of tools to manage electronic versions of the paper-based forms.

}, author = {Javier Lopez and Antonio Mana and Jose A. Montenegro and Juan J. Ortega and Jose M. Troya} } @inproceedings {JavierLopez2002a, title = {Verification of Authentication Protocols using SDL-method}, booktitle = {First International Workshop on Security in Information Systems (SIS{\textquoteright}02)}, year = {2002}, month = {April}, pages = {61-71}, address = {Ciudad Real, Spain}, abstract = {

Authentication between protocol agents is widely studied in the cryptographic protocol analysis area. It is essential in a virtual environment to rely on protocol parties{\textquoteright} identity. In the academic literature there are many protocols that provide the authentication property. We present in this paper a new mechanism to verify authentication using SDL, general purpose specification language. We have defined a generic schema in SDL that allow us to specify a security system and check system behavior when a malicious agent ( the intruder ) is present. We have used the EKE authentication protocol to illustrate how the mechanism works.

}, author = {Javier Lopez and Juan J. Ortega and Jose M. Troya} } @inproceedings {JavierLopez2000, title = {Aspectos de Implementaci{\'o}n de una Infraestructura de Clave P{\'u}blica Distribuida}, booktitle = {Simposio Espa{\~n}ol de Inform{\'a}tica Distribuida (SEID{\textquoteright}00)}, year = {2000}, month = {Septiembre}, pages = {313-320}, address = {Orense, Espa}, abstract = {

La seguridad es uno de los aspectos m\ás conflictivos del uso de Internet. La falta de una pol\ítica de seguridad global est\á frenando el desarrollo de Internet en \áreas tan interesantes y prometedoras como el comercio electr\ónico o la interacci\ón con las administraciones p\úblicas. Las t\écnicas criptogr\áficas actuales proporcionan un alto grado de confidencialidad; no obstante, es dif\ícil garantizar la identificaci\ón segura de los usuarios y, adem\ás, la gesti\ón de las claves de los mismos es poco eficiente y presenta graves problemas de escalabilidad. Este trabajo describe las caracter\ísticas de implementaci\ón de una soluci\ón a ambos problemas basada en una Infraestructura de Clave P\ública (PKI) que proporciona una administraci\ón simple y eficiente de las claves de los usuarios y posibilita la autenticaci\ón segura de los mismos.

}, author = {Javier Lopez and Antonio Mana and Jose A. Montenegro and Juan J. Ortega and Jose M. Troya} } @inproceedings {1721, title = {Development of Secure Internet Applications for Governmental Environments}, booktitle = {IEEE International Workshop on Electronic Government (in DEXA{\textquoteright}00)}, year = {2000}, pages = {362-365}, publisher = {IEEE Press}, organization = {IEEE Press}, isbn = {0-7695-0680-1}, author = {Jorge Davila and Javier Lopez and Antonio Mana and Juan J. Ortega and Jose maria troya} } @inproceedings {JavierLopez2000a, title = {Distributed Storage and Revocation in Digital Certificate Databases}, booktitle = {11th International Conference on Database and Expert Systems Applications (DEXA{\textquoteright}00)}, series = {LNCS}, volume = {1873}, year = {2000}, month = {September}, pages = {929-938}, publisher = {Springer}, organization = {Springer}, address = {London, U.K.}, abstract = {

Public-key cryptography is fast becoming the foundation for those applications that require security and authentication in open networks. But the widespread use of a global public-key cryptosystem requires that public-key certificates are always available and up-to-date. Problems associated to digital certificates management, like storage, retrieval, maintenance, and, specially, revocation, require special procedures that ensure reliable features because of the critical significance of inaccuracies. Most of the existing systems use a Certificate Revocation List, a repository of certificates that have been revoked before their expiration date. The need to access CRLs in order to check certificate revocations becomes a performance handicap. Furthermore, they introduce a source of vulnerability in the whole security infrastructure, as it is impossible to produce a new CRL each time a revocation takes place. This paper introduces an alternative for the storage of digital certificates that avoids the use of CRLs. The system is designed to provide a distributed management of digital certificates by using Certification Authorities that, while being part of a whole Public-Key Infrastructure, operate over local certificates databases. Communication protocols between local databases have been designed to minimize network traffic without a lack of security and efficiency.

}, author = {Javier Lopez and Antonio Mana and Juan J. Ortega and Jose M. Troya} } @inproceedings {JavierLopez1999c, title = {Cert{\textquoteright}eM: Certification System Based on Electronic Mail Service Structure}, booktitle = {Secure Networking (CQRE{\textquoteright}99)}, series = {LNCS}, volume = {1740}, year = {1999}, month = {December}, pages = {109-118}, publisher = {Springer}, organization = {Springer}, abstract = {

Public-Key Infrastructures are considered the basis of the protocols and tools needed to guarantee the security demanded for new Internet applications like electronic commerce, government-citizen relationships and digital distribution. This paper introduces a new infrastructure design, Cert{\textquoteright}eM, a key management and certification system that is based on the structure of the electronic mail service and on the principle of near-certification. Cert{\textquoteright}eM provides secure means to identify users and distribute their public-key certificates, enhances the efficiency of revocation procedures, and avoids scalability and synchronization problems. The system, developed and tested at the University of Malaga, was recently selected by RedIRIS, the National Research and Academic Network in Spain, to provide the public key service for its secure electronic mail.

}, author = {Javier Lopez and Antonio Mana and Juan J. Ortega} } @inproceedings {JavierLopez1999a, title = {A Public Key Infrastructure for User Identification}, booktitle = {IFIP Working Conference on User Identification and Privacy Protection}, year = {1999}, month = {June}, pages = {209-227}, address = {Stockholm, Sweden}, abstract = {

While there is wide agreement on the immense potential of Internet, its growth and performance are adversely affected by security issues. Despite its impressive size, scope and reach, the Internet has not yet become a common vehicle for many of these new possibilities. Progress in fields as electronic commerce and government-citizen relationships have been limited by the open design of the network itself. Today, Public-Key Infrastructures are the basis of the protocols and tools needed to guarantee the security demanded in those fields. Trust management and user identification are also important issues that remain unresolved. This paper introduces a key management and user identification system, named Cert\’eM, that is based on the electronic mail service. Cert{\textquoteright}eM provides important advantages over existing Public-Key Infrastructures and user identification proposals.

}, author = {Javier Lopez and Antonio Mana and Juan J. Ortega} } @inproceedings {JavierLopez1999b, title = {An User Authentication Infrastructure for Extranet Applications}, booktitle = {IEEE International Carnahan Conference on Security Technology}, year = {1999}, month = {October}, pages = {354-362}, publisher = {IEEE Press}, organization = {IEEE Press}, address = {Madrid, Spain}, abstract = {

An Extranet is used to connect businesses with their suppliers, customers or other businesses that share common goals in a way that automates their administrative interactions using Internet technology. The security of the communications over Internet is considered an essential feature. To guarantee secure operation the aid of some user authentication infrastructure is needed. This paper introduces a Public Key Infrastructure (PKI) and user identification scheme to be used in extranet applications. The flexibility of the system allows it to fit the usual hierarchical organization structure.

}, author = {Javier Lopez and Antonio Mana and Juan J. Ortega} } @article {JavierLopez1998, title = {Una Soluci{\'o}n Integral para la Autenticaci{\'o}n de Usuarios y la Administraci{\'o}n de Claves en Internet}, journal = {Nov{\'a}tica}, volume = {134}, year = {1998}, pages = {20-26}, abstract = {

La seguridad es uno de los aspectos m\ás conflictivos del uso de Internet. La falta de una pol\ítica de seguridad global est\á frenando el desarrollo de Internet en \áreas tan interesantes y prometedoras como el comercio electr\ónico o la interacci\ón con las administraciones p\úblicas. Las t\écnicas criptogr\áficas actuales proporcionan un alto grado de confidencialidad; no obstante, es dif\ícil garantizar la identificaci\ón segura de los usuarios y, adem\ás, la gesti\ón de las claves de los mismos es poco eficiente y presenta graves problemas de escalabilidad y seguridad. En este trabajo se describe una soluci\ón a ambos problemas basada en una Infraestructura de Clave P\ública que proporciona una administraci\ón simple y eficiente de las claves de los usuarios y posibilita la autenticaci\ón segura de los mismos. El sistema se ha probado con \éxito de forma local y, en breve, ser\á instalado para su prueba por parte de la comunidad de usuarios de RedIris.

}, issn = {0211-2124}, author = {Javier Lopez and Antonio Mana and Juan J. Ortega and Lucia Pino} } @inproceedings {AntonioMana1997, title = {Incremento de la Seguridad del Estandar de Cifrado de Datos basado en la Combinaci{\'o}n de Datos y Clave}, booktitle = {III Jornadas de Inform{\'a}tica y Autom{\'a}tica}, year = {1997}, month = {Julio}, pages = {423-432}, address = {El Puerto de Santa Mar{\'\i}a, Espa}, abstract = {

A pesar del gran esfuerzo investigador llevado a cabo, el ataque al DES ha sido infructuoso desde que a mediados de los setenta fue adoptado como est\ándar por el U. S. National Bureau of Standards. El criptoan\álisis diferencial constituye la base de las primeras t\écnicas capaces de acabar con tal invulnerabilidad. Las t\écnicas de criptoan\álisis basadas en modelos de fallos y su adaptaci\ón a DES, el criptoan\álisis de fallos diferencial, son dos de esas t\écnicas que han conseguido recientemente romper sistemas DES (aunque el ataque est\á limitado a ciertos casos especiales, en particular implementaciones hardware). En este art\ículo se presenta un punto d\ébil de DES sobre el cual puede aumentarse la seguridad y se propone una modificaci\ón de la estructura interna de DES con objeto de mejorar su resistencia ante el criptoan\álisis diferencial y por ende de los ataques derivados de este. La modificaci\ón introducida no supone un coste adicional elevado

}, author = {Antonio Mana and Javier Lopez and Lucia Pino and Juan J. Ortega and Carlos Maraval} } @inproceedings {1741, title = {Sistema Jer{\'a}rquico de Administraci{\'o}n de Claves P{\'u}blicas para el Correo Electr{\'o}nico}, booktitle = {I Jornadas de Ingenier{\'\i}a Telem{\'a}tica (JITEL{\textquoteright}97)}, year = {1997}, month = {Sep 1997}, pages = {295-302}, address = {Bilbao (Spain)}, isbn = {84-89654-04-2}, author = {Lucia Pino and Antonio Mana and Juan J. Ortega and Javier Lopez} }