Ciencias Exactas y Ciencias de la Salud
Permanent URI for this collectionhttps://hdl.handle.net/11285/551039
Pertenecen a esta colección Tesis y Trabajos de grado de las Maestrías correspondientes a las Escuelas de Ingeniería y Ciencias así como a Medicina y Ciencias de la Salud.
Browse
Search Results
- Verificación formal de protocolos de seguridad en HOL a partir del método inductivo(Instituto Tecnológico y de Estudios Superiores de Monterrey, 2003) López Pimentel, Juan Carlos; Monroy Borja, Raúl; Sánchez Velázquez, Erika; Rodríguez Lucatero, CarlosMuchos protocolos de seguridad han presentado fallas sutiles que han sido descubiertos a través de los métodos formales. De ahí que la principal razón por formalizarlos es para eliminar errores humanos. Sin embargo, muchos modelos se han limitado en demostrar sólo propiedades de autentificación. Ahora por la enorme cantidad de transacciones electrónicas y por personas malignas en la red, necesitamos métodos más potentes que también permitan verificar propiedades como confidencialidad, frescura y posibilidad. Uno de ellos es el Método inductivo desarrollado por Lawrence C. Paulson [ 16]. Sin embargo, este método está orientado a una comunidad específica (usuarios de Isabelle). La principal motivación para desarrollar el presente trabajo es proporcionar el método inductivo de Paulson a otra gran comunidad de usuarios que utilizan la herramienta del Sistema HOL1 [20, 40]. Con esto lograremos popularizar el método para que mayor número de usuarios puedan utilizar la verificación formal de protocolos de seguridad en HOL a partir del método inductivo. El método inductivo se basa específicamente de cuatro teorías: la de mensajes, eventos, llaves compartidas y llaves públicas. La teoría de mensajes contiene la definición de los tipos de agentes, de los mensajes, tipos de operadores para modelar el tráfico existente en la red. La teoría de eventos, contiene la definición de los tipos de eventos que pueden suceder al enviar un mensaje por la red o al recibirlos. Se modela el conocimiento de cada uno de los tipos de agentes y la frescura de los mensajes. Las teorías de llaves compartidas y llaves públicas proporcionan propiedades del conocimiento inicial de los agentes, características propias de las llaves y garantías sobre el suministro de llaves. Cada una de las teorías contiene propiedades específicas y son representados en forma de teoremas matemáticos. Al finalizar cada una de las teorías desarrolladas en HOL, hemos verificado el protocolo OtwayRees, demostrando entre otras propiedades autenticación. Por último, se dan las conclusiones y los trabajos futuros propuestos para la continuidad de este trabajo.
- Modelo de un sistema inmunológico natural en álgebra de procesos(Instituto Tecnológico y de Estudios Superiores de Monterrey, 2002) Saab Asbun, Rosa; Monroy Borja, Raúl; Vallejo Clemente, Edgar Emmanuel; Coello Coello, Carlos
- Sistema de monitoreo experto aplicado a equipos de cómputo(Instituto Tecnológico y de Estudios Superiores de Monterrey, 2000) Castro Loera, Arturo Rodolfo; ARTURO RODOLFO CASTRO LOERA:3176042; Monroy Borja, Raúl; González, Marco; Vázquez, Jesús; Camargo, FranciscoLa administración de servicios de cómputo se enfoca principalmente a mantenerlos en operación continua. Por eso gran parte del tiempo del administrador se enfoca principalmente al monitoreo, o la revisión de los servicios de cómputo para garantizar su funcionamiento correcto la mayor parte del tiempo. Existen muchas herramientas que ayudan al administrador a realizar esta labor, sobre todo, cuando el administrador no está presente para solucionar un problema de mal funcionamiento del servicio. No existe la herramienta perfecta para un monitoreo efectivo, por eso en esta tesis presentamos una solución que puede ayudar a la labor de monitoreo del administrador. La idea es obtener la experiencia de administradores expertos en un sistema de cómputo dado y administrar ese conocimiento para realizar un monitoreo efectivo, tal y como lo haría el propio administrador. Este conocimiento puede aplicarse en otros sistemas de cómputo similares, ya que solo es el conocimiento lo que se está aplicando.
- Reconocimiento de patrones aplicado a la exposición fotográfica(Instituto Tecnológico y de Estudios Superiores de Monterrey, 1999) Navarrete Paredes, Enrique Alejandro; ENRIQUE ALEJANDRO NAVARRETE PAREDES; García García, Eduardo de Jesús; Monroy Borja, Raúl; emipsanchez; Corona Burgueño, Juan Francisco; Vallejo Clemente, Edgar EmmanuelLa exposición fotográfica es un problema complejo que aún las cámaras fotográficas más sofisticadas (sistemas de zonas con forma predefinida) no resuelven satisfactoriamente en todos los casos. En esta tesis se desarrolla un sistema capaz de calcular la exposición fotográfica para escenas de tipo "paisaje" extrayendo las características de la imagen para alimentar una red neuronal. La extracción de los datos característicos de la imagen se hace mediante una segmentación de la misma, para obtener regiones con la forma de los elementos que componen la escena. Se hacen conjuntos de patrones (validación y entrenamiento) en función de la entropía de cada imagen. Estos conjuntos se usan para el proceso de entrenamiento y validación de la red neuronal. Se emplea el método de entrenamiento "Propagación hacia atrás con momentum y eliminación de punto plano".