安全协议的形式化分析技术与方法

对于安全协议的形式化分析方法从技术特点上做了分类和分析．对于安全协议分析技术的发展历史、目前的状况以及将来的趋势作了总体的介绍和总结．根据作者的体会，从纵向和横向两个角度进行了总结．纵向方面主要是从用于分析安全协议的形式化方法的出现和发展的历史角度加以总结．横向方面主要从所应用的技术手段、技术特点入手，进行总结分析．说明了目前协议形式化分析发展的主要方向．对于目前国际流行的方法和模型进行了例解．

对几类重要网络安全协议形式模型的分析

该文根据建模基础的不同,对目前处在研究热点中的几个重要协议形式模型进行了分类分析.它们可以分为4类:基于知识演化系统的模型;基于规则推理系统的模型;基于代数演算系统的模型及基于计算复杂性理论的模型.对每类模型作者提出了相应的抽象特征体系,并在该体系下分析了有代表性的模型,指出了这些模型的优缺点及进一步改进的思路.抽象体系的提出不仅使模型的本质变得清晰,而且还使同类模型中的不同模型之间的联系变得易于理解;分析了不同类型模型之间可能存在的联系,特别是用基于规则推理的模型的思路改进了Woo-Lam模型,在提出B模型抽象结构的同时,分析指出它极有可能发展成为一个统一各类模型的模型.

运用ASM描述安全协议

介绍了抽象状态机（ASM）,建立了基于这种形式化方法的协议描述于验证的环境,并建立了一般意义上的入侵者模型.作为应用实例,给出了 Helsinki协议的 ASM规约,说明利用这个规约可以直观的演绎 Horng-Hsu攻击.

Performance Analysis of Novel Randomly Shifted Certification Authority Authentication Protocol for MANETs

The provision of security in mobile ad hoc networks is of paramount importance due to their wireless nature. However, when conducting research into security protocols for ad hoc networks it is necessary to consider these in the context of the overall system. For example, communicational delay associated with the underlying MAC layer needs to be taken into account. Nodes in mobile ad hoc networks must strictly obey the rules of the underlying MAC when transmitting security-related messages while still maintaining a certain quality of service. In this paper a novel authentication protocol, RASCAAL, is described and its performance is analysed by investigating both the communicational-related effects of the underlying IEEE 802.11 MAC and the computational-related effects of the cryptographic algorithms employed. To the best of the authors' knowledge, RASCAAL is the first authentication protocol which proposes the concept of dynamically formed short-lived random clusters with no prior knowledge of the cluster head. The performance analysis demonstrates that the communication losses outweigh the computation losses with respect to energy and delay. MAC-related communicational effects account for 99% of the total delay and total energy consumption incurred by the RASCAAL protocol. The results also show that a saving in communicational energy of up to 12.5% can be achieved by changing the status of the wireless nodes during the course of operation. Copyright (C) 2009 G. A. Safdar and M. P. O'Neill (nee McLoone).

Practical Lattice-Based Digital Signature Schemes

Digital signatures are an important primitive for building secure systems and are used in most real-world security protocols. However, almost all popular signature schemes are either based on the factoring assumption (RSA) or the hardness of the discrete logarithm problem (DSA/ECDSA). In the case of classical cryptanalytic advances or progress on the development of quantum computers, the hardness of these closely related problems might be seriously weakened. A potential alternative approach is the construction of signature schemes based on the hardness of certain lattice problems that are assumed to be intractable by quantum computers. Due to significant research advancements in recent years, lattice-based schemes have now become practical and appear to be a very viable alternative to number-theoretic cryptography. In this article, we focus on recent developments and the current state of the art in lattice-based digital signatures and provide a comprehensive survey discussing signature schemes with respect to practicality. Additionally, we discuss future research areas that are essential for the continued development of lattice-based cryptography.

Probabilistic reasoning of inconsistent belief in protocol analysis

Security protocols have been recently found with subtle flaws due to incomplete or ambiguous specification. Although formal methods have remarkably assisted in protocol analysis, they ignores the effect of hostile/uncertain environment, which might lead to inconsistent belief that can be held by principals in delivered messages. This discrepant belief may prevent us from representing the insecurity and uncertainty in a real trading situation. Unfortunately, the current approaches lack the ability to handle the inconsistent belief. This article presents a probabilistic method, which intuitively measures the belief from different principals that can be put on the goal of the protocol. The experiments demonstrate our method is useful to enhance the protocol analysis.

Agents based e-commerce and securing exchanged information

Mobile agents have been implemented in e-commerce to search and filter information of interest from electronic markets. When the in format ion is very sensitive and critical, it is important to develop a novel security protocol that can efficiently protect the information from malicious tampering as well as unauthorized disclosure or at least detect any malicious act of intruders. In this chapter, we describe robust security techniques that ensure a sound security of information gathered throughout agent's itinerary against various security attacks, as well as truncation attacks. A sound security protocol is described , which implements the various security techniques that would jointly prevent or at least detect any malicious act of intruders. We reason about the soundness of the protocol using Symbolic Trace Analyzer (STA), a formal verification tool that is based on symbolic techniques. We analyze the protocol in key configurations and show that it is free of flaws. We also show that the protocol fulfils the various security requirements of exchanged information in MAS, including data-integrity, data-confidentiality, data authenticity, origin confidentiality and data non-repudiability.

A hybrid mutual authentication protocol for RFID

Out of the large number of RFID security protocols proposed in recent years none have proven to be truly secure and the creation of a truly secure security protocol for systems employing low cost RFID tags remains an open problem. In this paper we develop and present a RFID security protocol which not only allows mutual authentication and secure transmission of data between the reader and tag but is also secure against a number of common attacks.

A robust grouping proof protocol for RFID EPC C1G2 tags

Several grouping proof protocols for RFID systems have been proposed over the years but they are either found to be vulnerable to certain attacks or do not comply with the EPC class-1 gen-2 (C1G2) standard because they use hash functions or other complex encryption schemes. Among other requirements, synchronization of keys, simultaneity, dependence, detecting illegitimate tags, eliminating unwanted tag processing, and denial-of-proof attacks have not been fully addressed by many. Our protocol addresses these important gaps by taking a holistic approach to grouping proofs and provides forward security, which is an open research issue. The protocol is based on simple (XOR) encryption and 128-bit pseudorandom number generators, operations that can be easily implemented on low-cost passive tags. Thus, our protocol enables large-scale implementations and achieves EPC C1G2 compliance while meeting the security requirements.

Secure ownership transfer for multi-tag multi-owner passive RFID environment with individual-owner-privacy

In this paper we propose a secure ownership transfer protocol for a multi-tag multi-owner RFID environment that provides individual-owner-privacy. To our knowledge, the existing schemes do not provide individual-owner-privacy and most of the existing schemes do not comply with the EPC Global Class-1 Gen-2 (C1G2) standard since the protocols use expensive hash operations or sophisticated encryption schemes that cannot be implemented on low-cost passive tags that are highly resource constrained. Our work aims to fill these gaps by proposing a protocol that provides individual-owner-privacy, based on simple XOR and 128-bit pseudo-random number generators (PRNG), operations that are easily implemented on low-cost RFID tags while meeting the necessary security requirements thus making it a viable option for large scale implementations. Our protocol also provides additional protection by hiding the pseudo-random numbers during all transmissions using a blind-factor to prevent tracking attacks.

Securing sensor networks by moderating frequencies

Security of Wireless Sensor Network (WSN) is a key issue in information security. Most existing security protocols exploit various Mathematical tools to strengthen their security. Some protocols use the details of the geographical location of the nodes. However, to the best authors’ knowledge, none of the existing works exploit the constraints faced by the adversary, specifically, tracing a particular frequency from a large range of unknown frequency channels. The current work uses positional details of the individual nodes. Then the aim is to exploit this weakness of tracing frequencies by assigning a wide range of frequency channels to each node. Experiments using Magneto Optic Sensors reveal that any change of the parametric Faraday’s rotational angle affects the frequency of the Optical waves. This idea can perhaps be generalized for practically deployable sensors (having respective parameters) along with a suitable key management scheme.

Certificados electrónicos de servidor en administración y comercio electrónicos: garantías de seguridad

El uso de Internet por parte de los ciudadanos para relacionarse con las Administraciones Públicas o en relación con actividades de comercio electrónico crece día a día. Así lo evidencian los diferentes estudios realizados en esta materia, como los que lleva a cabo el Observatorio Nacional de las Telecomunicaciones y la Sociedad de la Información (http://www.ontsi.red.es/ontsi/). Se hace necesario, por tanto, identificar a las partes intervinientes en estas transacciones, además de dotarlas de la confidencialidad necesaria y garantizar el no repudio. Uno de los elementos que, junto con los mecanismos criptográficos apropiados, proporcionan estos requisitos, son los certificados electrónicos de servidor web. Existen numerosas publicaciones dedicadas a analizar esos mecanismos criptográficos y numerosos estudios de seguridad relacionados con los algoritmos de cifrado, simétrico y asimétrico, y el tamaño de las claves criptográficas. Sin embargo, la seguridad relacionada con el uso de los protocolos de seguridad SSL/TLS está estrechamente ligada a dos aspectos menos conocidos:  el grado de seguridad con el que se emiten los certificados electrónicos de servidor que permiten implementar dichos protocolos; y  el uso que hacen las aplicaciones software, y en especial los navegadores web, de los campos que contiene el perfil de dichos certificados. Por tanto, diferentes perfiles de certificados electrónicos de servidor y diferentes niveles de seguridad asociados al procedimiento de emisión de los mismos, dan lugar a diferentes tipos de certificados electrónicos. Si además se considera el marco jurídico que afecta a cada uno de ellos, se puede concluir que existe una tipología de certificados de servidor, con diferentes grados de seguridad o de confianza. Adicionalmente, existen otros requisitos que también pueden pasar desapercibidos tanto a los titulares de los certificados como a los usuarios de los servicios de comercio electrónico y administración electrónica. Por ejemplo, el grado de confianza que otorgan los navegadores web a las Autoridades de Certificación emisoras de los certificados y cómo estas adquieren tal condición, o la posibilidad de poder verificar el estado de revocación del certificado electrónico. El presente trabajo analiza todos estos requisitos y establece, en función de los mismos, la correspondiente tipología de certificados electrónicos de servidor web. Concretamente, las características a analizar para cada tipo de certificado son las siguientes:  Seguridad jurídica.  Normas técnicas.  Garantías sobre la verdadera identidad del dominio.  Verificación del estado de revocación.  Requisitos del Prestador de Servicios de Certificación. Los tipos de certificados electrónicos a analizar son:  Certificados de servidor web:  Certificados autofirmados y certificados emitidos por un Prestador de Servicios de Certificación.  Certificados de dominio simple y certificados multidominio (wildcard y SAN)  Certificados de validación extendida.  Certificados de sede electrónica. ABSTRACT Internet use by citizens to interact with government or with e-commerce activities is growing daily. This topic is evidenced by different studies in this area, such as those undertaken by the Observatorio Nacional de las Telecomunicaciones y la Sociedad de la Información (http://www.ontsi.red.es/ontsi/ ). Therefore, it is necessary to identify the parties involved in these transactions, as well as provide guaranties such as confidentiality and non-repudiation. One instrument which, together with appropriate cryptographic mechanisms, provides these requirements is SSL electronic certificate. There are numerous publications devoted to analyzing these cryptographic mechanisms and many studies related security encryption algorithms, symmetric and asymmetric, and the size of the cryptographic keys. However, the safety related to the use of security protocols SSL / TLS is closely linked to two lesser known aspects:  the degree of security used in issuing the SSL electronic certificates; and  the way software applications, especially web Internet browsers, work with the fields of the SSL certificates profiles. Therefore, the diversity of profiles and security levels of issuing SSL electronic certificates give rise to different types of certificates. Besides, some of these electronic certificates are affected by a specific legal framework. Consequently, it can be concluded that there are different types of SSL certificates, with different degrees of security or trustworthiness. Additionally, there are other requirements that may go unnoticed both certificate holders and users of e-commerce services and e-Government. For example, the degree of trustworthiness of the Certification Authorities and how they acquire such a condition by suppliers of Internet browsers, or the possibility to verify the revocation status of the SSL electronic certificate. This paper discusses these requirements and sets, according to them, the type of SSL electronic certificates. Specifically, the characteristics analyzed for each type of certificate are the following:  Legal security.  Technical standards.  Guarantees to the real identity of the domain.  Check the revocation status.  Requirements of the Certification Services Providers. The types of electronic certificates to be analyzed are the following:  SSL electronic certificates:  Self-signed certificates and certificates issued by a Certification Service Provider.  Single-domain certificates and multi-domain certificates (wildcard and SAN)  Extended Validation Certificates.  “Sede electrónica” certificates (specific certificates for web sites of Spanish Public Administrations).

Redes VSAT con el estándar DVB-S

Actualmente las redes VSAT (Very Small Aperture Terminal) están adquiriendo una mayor importancia en las comunicaciones por satélite debido a las nuevas aplicaciones que se están desarrollando tanto a nivel empresarial como a nivel de usuario final. El presente proyecto pretende hacer un estudio de este tipo de red para presentarla como una solución al problema de querer conectar estaciones dispersas, que por el perfil del terreno hace difícil la conexión de las mismas a través de las redes terrestres convencionales. Los nuevos estándares están haciendo que este tipo de redes proliferen muy deprisa ya que se consigue una mayor flexibilidad que con los estándares precedentes para este tipo de red. En concreto, en este proyecto se ha estudiado el estándar abierto DVB-S desarrollado por el grupo de trabajo DVB por ser uno de los más aceptado internacionalmente. Para comprender este sistema de comunicaciones, el proyecto está estructurado en dos partes. En la primera parte se hace una revisión de cómo han evolucionado las comunicaciones satelitales VSAT, indicando las ventajas y desventajas de su implementación y sobre todo la orientación que éstas muestran a la utilización de los estándares DVB. Posteriormente se realiza un estudio de los estándares DVB-S y DVBRCS en donde se profundiza en conceptos claves tales como el Multiplexado de Transporte MPEG-2, los mecanismos de envío de mensajes de señalización, etc. En la segunda parte del proyecto se presta atención a la seguridad de la red, analizando los mecanismos propios que presenta el estándar DVB así como los diferentes protocolos de seguridad existentes en las capas superiores para una protección adicional. Para concluir el proyecto se han creado dos aplicaciones, la primera como método didáctico para comprender mejor el comportamiento de las redes VSAT con el estándar DVB-S, y una segunda aplicación con carácter comercial para la transferencia de ficheros de manera segura con características específicas, enfocada particularmente en redes VSAT, aunque siendo posible su uso en otras redes. ABSTRACT. Nowadays VSAT networks (Very Small Aperture Terminal) are becoming more important in satellite communications, due to several new applications that are being developed both at company level and end user level. This project aims to make a study of this type of network to present it as a solution to the problem of wanting to connect scattered stations, because the terrain profile makes difficult to connect them via conventional terrestrial networks. New standards are making that such networks proliferate very quickly for the reason that a more flexibility than the previous standards for this type of network is achieved. Specifically, this project has studied the open standard DVB-S developed by the DVB workgroup as one of the most internationally accepted. To understand this communication system, this project is structured in two different parts: On one hand, in the first part a review about how VSAT satellite communications have evolved, indicating the advantages and disadvantages of its implementation and above all, the guidance that they show to the use of the DVB standards. Subsequently, a study of the DVB-S and DVB-RCS standards is developed, where delves into key concepts such as MPEG-2 Multiplexed Transport, mechanisms of transmission of signaling messages, etc. On the other hand, in the second part of the project, we focus on network security, analyzing the mechanisms presented by the DVB standard and various existing security protocols in the upper layers for an extra protection. To complete the project two different applications have been developed: the first one as a teaching method to better understand the behavior of VSAT networks in DVB-S standard, and the second one with a commercial basis for transferring files securely with specific features applications focused particularly in VSAT networks, although with a possible use on other networks.