No description available.

La agricultura es una de las prácticas humanas más antiguas y de mayor importancia en nuestra sociedad. Es fundamental para la subsistencia de millones de personas, donde cultivos como el arroz o el trigo son la base alimenticia de un gran porcentaje de la población mundial. Al igual que la sociedad, las técnicas agrícolas han ido evolucionando con el paso del tiempo. En este contexto, es la agricultura de precisión el tipo de agricultura que más fuerza y mejores resultados está obteniendo. La agricultura de precisión surge con la aplicación de nuevos elementos tecnológicos con el objetivo de optimizar la gestión de una parcela desde el punto de vista: • Agronómico: ajuste de las prácticas de cultivo a las necesidades de la planta • Medioambiental: reducción del impacto vinculado a la actividad agrícola • Económico: aumento de la competitividad a través de una mayor eficacia de las prácticas. Una de las medidas más utilizadas en la inspección del estado de los cultivos es la de medida del estado fenológico (fenología). La fenología nos indica las diferentes etapas biológicas que irá atravesando un cultivo desde su siembra hasta la cosecha. El conocimiento exacto de este valor es fundamental en las prácticas agrícolas, dado que marca el momento en el que se debe realizar cada uno de los procesos agrícolas. Por ejemplo, el momento del suministro de nutrientes como el nitrógeno, es uno de los aspectos claves en el incremento de la productividad y de no aplicarse en el estado fenológico correcto la productividad en vez de aumentar se verá reducida. Una de las formas que tenemos para inferir el valor fenológico es mediante teledetección. La utilización de satélites nos permite cubrir grandes extensiones de terreno en un mismo instante de tiempo. En este contexto las fuentes de observación más utilizadas son de naturaleza radar (en concreto SAR) e imágenes ópticas. Ambas poseen características diferentes y ofrecen distintas sensibilidades. Por ejemplo, el sensor óptico es sensible a los procesos químicos internos de las plantas y el SAR a su estructura o morfología. La forma más extendida para la estimación fenológica a partir de las series de datos sensoriales se basa en el procesado de señal convencional. Por ejemplo, para el caso del sistema SAR se puede analizar la evolución de determinados parámetros polarimétricos en función del estado del cultivos y en base a este análisis definir una estrategia de estimación Por otro lado, el sensor óptico ha sido el más utilizado para dicho fin. A partir de una combinación de bandas ópticas se definen unos índices denominados Índices de Vegetación (IV). Estos índices maximizan su respuesta ante la presencia de vegetación y se ven minimizados ante cualquier otro tipo de terreno. Dentro de los diferentes IV el más estudiado es el Índice de vegetación de diferencia normalizada o NDVI (de sus siglas en inglés). El NDVI debe ser filtrado antes de ser utilizado para estimar el estado fenológico debido al ruido inherente de los datos ópticos. Las técnicas convencionales utilizan métodos basados en ajustes o transformadas que requieren todo el set de imágenes (durante toda la campaña) para poder trabajar, lo cual imposibilita el uso de estas técnicas en aplicaciones de tiempo real. Otro de los inconvenientes es que debido a la poca sensibilidad que tiene el NDVI entre cambios fenológicos solo se pueden distinguir unos pocos estados Dando un enfoque diferente, un enfoque dinámico, podemos ofrecer estimaciones mucho más robustas que las obtenidas hasta ahora. El enfoque dinámico analiza no sólo el contenido de los datos sensoriales sino también su evolución temporal. Para esto, no se parte directamente de los datos observados sino que se divide el problema en dos etapas: 1. Modelo del comportamiento del sistema que determina su evolución temporal permitiendo predecir las transiciones entre dos instantes de tiempo. 2. Inclusión de los datos procedentes de la observación (sensores radar y/u ópticos). La primera etapa consiste en la utilización de un modelo que describe el comportamiento temporal del sistema, en nuestro caso, la evolución fenológica a lo largo del tiempo, con el fin de realizar una predicción de hacia dónde evoluciona el siguiente estado. Esta predicción se combina en la siguiente etapa, con la observación proveniente de los sensores. Esto supone un gran avance respecto a los métodos en los que se deben desarrollar estudios y ajustes matemáticos para cada sensor por separado y determinar el estado basándonos única y exclusivamente en la información proporcionada por dicho sensor en un instante de tiempo. En estudios recientes se ha demostrado el potencial de la metodología sobre cultivos de arroz utilizando modelos de evolución fenológica combinados con imágenes SAR u observaciones ópticas. Otra posibilidad que brinda esta metodología es la fusión de datos, es decir, la segunda etapa puede albergar más de una fuente de observación que se combine con la predicción. Imaginemos un escenario de teledetección para el que disponemos de tres fuentes de información periódica: imágenes de satélite ópticas, radar y fotografías a pie de campo. El enfoque tradicional estudiaría la información de cada fuente por separado y proporcionaría una solución para cada una de las fuentes. Si utilizamos un enfoque dinámico lo que haremos es determinar una única solución combinando de forma óptima la información actual y pasada de los tres sensores. De este modo, aquellos estados en los que un sensor sea menos sensible pueden verse compensados por la información de otros sensores para mejorar la predicción. Uno de los factores claves para obtener buenos resultados utilizando esta metodología es disponer de un buen muestreo temporal. Una forma de reducir el tiempo de revisita (tiempo entre imágenes) es mediante el uso de un vehículo aéreo no tripulado (UAV) cuya incorporación no supone inconvenientes en esta metodología. Al contrario, facilita sustancialmente la transferencia de esta nueva tecnología a la sociedad. Los UAV, además de ser flexibles en la configuración del tiempo de adquisición, nos permiten observar los cultivos a la distancia que se desee. El vehículo es capaz de realizar la trayectoria sin necesidad de pilotarlo y además, aprovechar al máximo el enfoque dinámico para calcular las trayectorias de forma autónoma. Por ejemplo, si el vehículo detecta una zona que presenta incertidumbre o algún problema podría modificar su trayectoria para recabar más información de dicha zona. Este enfoque abre una nueva brecha de posibilidades y de aplicaciones que pueden ser transferidas del ámbito científico a la sociedad mediante la creación de nuevos productos comerciales.

Tesis por compendio / [ES] La herramienta criptográfica Maude-NPA es un verificador de modelos especializado para protocolos de seguridad criptográficos que tienen en cuenta las propiedades algebraicas de un sistema criptográfico. En la literatura, las propiedades criptográficas adicionales han descubierto debilidades de los protocolos de seguridad y, en otros casos, son parte de los supuestos de seguridad del protocolo para funcionar correctamente. Maude-NPA tiene una base teórica en la rewriting logic, la unificación ecuacional y el narrowing para realizar una búsqueda hacia atrás desde un patrón de estado inseguro para determinar si es alcanzable o no. Maude-NPA se puede utilizar para razonar sobre una amplia gama de propiedades criptográficas, incluida la cancelación del cifrado y descifrado, la exponenciación de Diffie-Hellman, el exclusive-or y algunas aproximaciones del cifrado homomórfico. En esta tesis consideramos nuevas propiedades criptográficas, ya sea como parte de protocolos de seguridad o para descubrir nuevos ataques. También hemos modelado diferentes familias de protocolos de seguridad, incluidos los Distance Bounding Protocols or Multi-party key agreement protocolos. Y hemos desarrollado nuevas técnicas de modelado para reducir el coste del análisis en protocolos con tiempo y espacio. Esta tesis contribuye de varias maneras al área de análisis de protocolos criptográficos y muchas de las contribuciones de esta tesis pueden ser útiles para otras herramientas de análisis criptográfico. / [CA] L'eina criptografica Maude-NPA es un verificador de models especialitzats per a protocols de seguretat criptogràfics que tenen en compte les propietats algebraiques d'un sistema criptogràfic. A la literatura, les propietats criptogràfiques addicionals han descobert debilitats dels protocols de seguretat i, en altres casos, formen part dels supòsits de seguretat del protocol per funcionar correctament. Maude-NPA te' una base teòrica a la rewriting lògic, la unificació' equacional i narrowing per realitzar una cerca cap enrere des d'un patró' d'estat insegur per determinar si es accessible o no. Maude-NPA es pot utilitzar per raonar sobre una amplia gamma de propietats criptogràfiques, inclosa la cancel·lació' del xifratge i desxifrat, l'exponenciacio' de Diffie-Hellman, el exclusive-or i algunes aproximacions del xifratge homomòrfic. En aquesta tesi, considerem noves propietats criptogràfiques, ja sigui com a part de protocols de seguretat o per descobrir nous atacs. Tambe' hem modelat diferents famílies de protocols de seguretat, inclosos els Distance Bounding Protocols o Multi-party key agreement protocols. I hem desenvolupat noves tècniques de modelització' de protocols per reduir el cost de l'analisi en protocols amb temps i espai. Aquesta tesi contribueix de diverses maneres a l’àrea de l’anàlisi de protocols criptogràfics i moltes de les contribucions d’aquesta tesi poden ser útils per a altres eines d’anàlisi criptogràfic. / [EN] The Maude-NPA crypto tool is a specialized model checker for cryptographic security protocols that take into account the algebraic properties of the cryptosystem. In the literature, additional crypto properties have uncovered weaknesses of security protocols and, in other cases, they are part of the protocol security assumptions in order to function properly. Maude-NPA has a theoretical basis on rewriting logic, equational unification, and narrowing to perform a backwards search from an insecure state pattern to determine whether or not it is reachable. Maude-NPA can be used to reason about a wide range of cryptographic properties, including cancellation of encryption and decryption, Diffie-Hellman exponentiation, exclusive-or, and some approximations of homomorphic encryption. In this thesis, we consider new cryptographic properties, either as part of security protocols or to discover new attacks. We have also modeled different families of security protocols, including Distance Bounding Protocols or Multi-party key agreement protocols. And we have developed new protocol modeling techniques to reduce the time and space analysis effort. This thesis contributes in several ways to the area of cryptographic protocol analysis and many of the contributions of this thesis can be useful for other crypto analysis tools. / This thesis would not have been possible without the funding of a set of research projects. The main contributions and derivative works of this thesis have been made in the context of the following projects: - Ministry of Economy and Business of Spain : Project LoBaSS Effective Solutions Based on Logic, Scientific Research under award number TIN2015-69175-C4-1-R, this project was focused on using powerful logic-based technologies to analyze safety-critical systems. - Air Force Office of Scientific Research of United States of America : Project Advanced symbolic methods for the cryptographic protocol analyzer Maude-NPA Scientific Research under award number FA9550-17-1-0286 - State Investigation Agency of Spain : Project FREETech: Formal Reasoning for Enabling and Emerging Technologies Scientific I+D-i Research under award number RTI2018-094403-B-C32 / Aparicio Sánchez, D. (2022). Modeling and Analysis of Advanced Cryptographic Primitives and Security Protocols in Maude-NPA [Tesis doctoral]. Universitat Politècnica de València. https://doi.org/10.4995/Thesis/10251/190915 / Compendio