Burcu Külahçioglu

Automi temporizzati come strumento di verifica per i protocolli di sicurezza

Un'analisi su un caso di studio

• Broschiertes Buch

Produktbeschreibung

Gli automi temporizzati sono un'estensione dell'approccio auto-teorico alla modellazione di sistemi in tempo reale che introduce il tempo negli automi classici. Da quando è stato proposto per la prima volta nei primi anni Novanta, è diventato un importante settore di ricerca ed è stato ampiamente studiato sia nel contesto dei linguaggi formali che della modellazione e della verifica dei sistemi in tempo reale. Gli automi temporizzati utilizzano la modellazione a tempo denso, consentendo un'efficiente verifica modellistica di sistemi sensibili al tempo il cui corretto funzionamento dipende dalle proprietà di temporizzazione. Una di queste aree di applicazione è la verifica dei protocolli di sicurezza. Questo libro si concentra sul modello degli automi temporizzati e lo utilizza come strumento di verifica dei protocolli di sicurezza. Come caso di studio, il protocollo di autenticazione ripetuto Neuman-Stubblebine Repeated Authentication Protocol viene modellato e verificato utilizzando le proprietà sensibili al tempo del modello. Vengono analizzati i difetti del protocollo e vengono commentati i vantaggi e le sfide del modello.

Produktdetails

• Verlag: Edizioni Sapienza
• Seitenzahl: 96
• Erscheinungstermin: 26. August 2021
• Italienisch
• Abmessung: 220mm x 150mm x 6mm
• Gewicht: 161g
• ISBN-13: 9786203133561
• ISBN-10: 6203133566
• Artikelnr.: 62512213

Autorenporträt

Burcu Külahç¿ölu, M.S.: Estudió la licenciatura en Ingeniería Informática en la Universidad de Yeditepe. Obtuvo el título de M.S. en el Instituto de Tecnología ¿zmir. Sus intereses de investigación incluyen la teoría de los autómatas temporizados, el modelado y la verificación de los sistemas en tiempo real y los fundamentos teóricos de la ciencia de la computación. Asistente de investigación en la Universidad de Yasar, Izmir.