Mixnets e EasyCrypt: dimostrazioni crittografiche assistite da calcolatore

Negli ultimi anni l'avanzamento della ricerca in campo crittografico ha portato alla necessità di utilizzare strumenti software per la verifica delle prove formali. EasyCrypt è un tool, in fase di sviluppo, ideato per dimostrazioni basate su sequenze di giochi. Nella presente tesi viene presentato un caso di studio riguardante l'applicabilità di EasyCrypt alle mixing networks (abbr. mixnets). è presente un'esaustiva rassegna delle mixnets proposte in letteratura ed è descritta la teoria alla base delle dimostrazioni critografiche basate su sequenze di giochi. EasyCrypt viene analizzato nei suoi fondamenti teorici nonché nelle applicazioni pratiche, con riferimento particolare agli esperimenti svolti per la dimostrazione di proprietà di sicurezza delle mixnets.

Un Framework per il controllo e la gestione automatica dello spostamento di sensori mobili

Il progetto descritto in questo documento consiste nello sviluppo di un Framework composto da un'applicazione Android in grado di comandare il movimento di un robot collegato ad una scheda Arduino tramite interfaccia di comunicazione Bluetooth

Sicurezza nelle reti di sensori wireless UWB: generazione di chiavi simmetriche da parametri fisici

Le reti di oggetti intelligenti costituiscono una realtà che si sta affermando nel mondo quotidiano. Dispositivi capaci di comunicare tra loro, oltre che svolgere la propria funzione primaria, possono comporre una nuvola che faccia riferimento al legittimo proprietario. Un aspetto fondamentale di questo scenario riguarda la sicurezza, in particolar modo per garantire una comunicazione protetta. Il soddisfacimento di questo requisito è fondamentale anche per altri punti come l'integrità dell'informazione condivisa e l'autenticazione. Lo strumento più antico e tutt'ora adatto alla riservatezza di una comunicazione è costituito dalla crittografia. Una tecnica crittografica è schematicamente composta da un algoritmo che, a seconda di una chiave e del messaggio in ingresso, restituisce in uscita un messaggio cifrato, il crittogramma. Questo viene poi inviato e al legittimo destinatario che, essendo in possesso della chiave e dell'algoritmo, lo converte nel messaggio originale. L'obiettivo è rendere impossibile ad un utente malevolo - non dotato di chiave - la ricostruzione del messaggio. L'assunzione che l'algoritmo possa essere noto anche a terze parti concentra l'attenzione sul tema della chiave. La chiave deve essere sufficientemente lunga e casuale, ma soprattutto deve essere nota ai due utenti che intendono instaurare la comunicazione. Quest'ultimo problema, noto come distribuzione della chiave, è stato risolto con il sistema RSA a chiave pubblica. Il costo computazionale di questa tecnica, specialmente in un contesto di dispositivi non caratterizzati da grandi potenze di calcolo, suggerisce però la ricerca di strade alternative e meno onerose. Una soluzione promettente ed attualmente oggetto di studio sembra essere costituita dalle proprietà del canale wireless. Un ponte radio è caratterizzato da una funzione di trasferimento che dipende dall'ambiente in cui ci si trova e, per il teorema di reciprocità, risulta essere lo stesso per i due utenti che l'hanno instaurato. Oggetto della tesi è lo studio ed il confronto di alcune delle tecniche possibili per estrarre una chiave segreta da un mezzo condiviso, come quello del canale wireless. Si presenterà il contesto in cui verrà sviluppato l'elaborato. Si affronteranno in particolare due casi di interesse, costituiti dalla attuale tecnologia di propagazione del segnale a banda stretta (impiegata per la maggior parte delle trasmissioni senza fili) per passare a quella relativamente più recente della banda Ultra-larga (UWB). Verranno poi illustrate delle tecniche per ottenere stringhe di bit dai segnali acquisiti, e saranno proposti dei metodi per la loro correzione da eventuali discordanze. Saranno infine riportate le conclusioni sul lavoro svolto e le possibili strade future.

Realizzazione di un sistema di traduzione automatica di regole semantiche dall'italiano al francese.

Nell’ambito di questo progetto di tesi è stato studiato un sistema per la traduzione automatica, dall'italiano al francese, del contenuto di regole semantiche. Le regole in oggetto riguardano la categorizzazione di documenti secondo la tassonomia definita da IPTC.

Analisi esplorativa e armonizzazione di dataset per la rappresentazione grafica mediante la libreria d3

L’idea alla base della tesi è quella di sfruttare l’espressività di rappresentazione grafica della libreria D3 per mettere a punto un’applicazione web che dia la possibilità all’utente di creare dei grafici interattivi in maniera semplice e automatica. A tal proposito, si è subito considerato il dominio dell’applicazione, rappresentato dai dati da visualizzare in forma grafica, in modo da sviluppare un prodotto che, a differenza degli altri generatori di grafici, permetta l’elaborazione dei dataset reali, quelli cioè pubblicati sul web dai vari enti specializzati; un’applicazione che quindi indipendentemente dalla forma in cui i dati si presentano, riesca a rappresentarne il contenuto.

Generazione automatica di visualizzazioni di open data quantitativi

Le sfide dell'Information Visualisation ed i limiti dei sistemi di visualizzazione esistenti hanno portato alla creazione di un nuovo sistema per la generazione automatica di visualizzazioni di Open Data quantitativi, presentato in questa tesi.

Il problema della primalità in complessità computazionale

Questa tesi vuole fornire un'introduzione alla complessità computazionale e allo studio dei numeri primi riferito a questa materia. Si tratterà della Macchina di Turing e della sua importanza per calcolabilità e complessità, introducendo le classi P ed NP. Queste saranno approfondite studiando prima la classe di problemi NP-completi e successivamente fornendo alcuni esempi importanti. Nella parte finale ci si occuperà esplicitamente del problema dei numeri primi e si guarderà da vicino l'algoritmo AKS, dimostrandone la correttezza.

Controllo del moto di una macchina automatica flessibile per il packaging

In questo studio viene sviluppato il controllo del moto di una macchina automatica per il packaging destinata a linee di media produttività con cambi formato rapidi. Il lavoro comprende la realizzazione di simulazioni dei gruppi macchina, la progettazione dei profili di moto da assegnare ai loro motori ed, infine, l'analisi dinamica e la verifica degli attuatori stessi.

Segmentazione automatica dell'atrio sinistro e valutazione della fibrosi atriale in risonanza magnetica

Questo lavoro di tesi si è svolto in collaborazione con le Unità Operative di Cardiologia e di Radiologia dell’ospedale “M. Bufalini” di Cesena e della St. Jude Medical, Inc., con l’obiettivo di sviluppare e implementare un metodo per l’identificazione e la valutazione della fibrosi atriale mediante risonanza magnetica in pazienti con fibrillazione atriale, candidati a procedura di ablazione. I pazienti sono stati sottoposti all’esame di risonanza magnetica (RM) angio per la valutazione della morfologia atriale e alla DE-MRI per l’identificazione e la visualizzazione delle zone di alto enhancement sulla struttura 3D dell’atrio sinistro, ossia le zone di alta intensità corrispondenti alla fibrosi. La struttura anatomica è utile all’elettrofisiologo per conoscere la morfologia dell’atrio e delle vene polmonari, permettendo quindi di minimizzare l’uso della fluoroscopia durante la procedura di ablazione. La conoscenza dei siti e della quantificazione della fibrosi è vantaggiosa per il medico per la pianificazione preoperatoria, in quanto nei pazienti con molta fibrosi non è sufficiente l’isolamento delle vene polmonari, ma si ottengono risultati migliori effettuando un’ablazione estensiva della parete atriale. Inoltre gli studi in letteratura hanno dimostrato che i pazienti con un’estensione di fibrosi superiore al 35% della superficie atriale, hanno una probabilità superiore al 50% di soffrire nuovamente di fibrillazione atriale dopo la procedura di ablazione; lo studio della fibrosi atriale vuole quindi essere un metodo per predire se l’ablazione avrà successo, oppure se è preferibile seguire indicazioni terapeutiche diverse. Il primo passo di questo lavoro è stata la registrazione delle immagini angio-RM e DE-MR mediante il software VolView. Successivamente si è implementato un programma in Matlab per segmentare in modo automatico l’atrio sinistro e si è visualizzata la struttura tridimensionale con la mappa cromatica della fibrosi utilizzando il software ParaView. Infine per validare questo lavoro si è effettuato un confronto qualitativo dei risultati ottenuti con il mappaggio elettro-anatomico acquisito mediante il sistema EnSite Velocity della St. Jude Medical, Inc. durante la procedura di ablazione transcatetere. Per eseguire questo confronto è stato necessario interfacciare il nostro lavoro con il sistema EnSite Velocity, con lo scopo di riuscire a visualizzare le mappe elettro-anatomiche sul nostro sistema e di importare la nostra struttura anatomica nel loro.