RICERCA ITALIANA     

SOFT - Tecniche formali orientate alla sicurezza

Università "Ca' Foscari" di Venezia

Abstract

La sicurezza dei sistemi software è una questione cruciale in un mondo sempre più permeato dall'Information Technology. Il numero di servizi, accessibili via reti di natura telematica, che aiutano ad affrontare attività quotidiane va aumentando, come testimoniato dal sempre crescente numero di espressioni come e-banking, e-commerce ed e-government, ove il prefisso 'e' ne sostanzia la dimensione elettronica. Tali servizi richiedono sia lo scambio di informazioni confidenziali che la condivisione di risorse computazionali e presentano forti requisiti di sicurezza, data la grande rilevanza delle informazioni trattate e il contesto fortemente distribuito e insicuro, quale è Internet, in cui esse tipicamente operano. Si rivela importante, ad esempio, stabilire l'autenticità dei messaggi scambiati, la loro segretezza, le identità delle parti in causa, e anche avere garanzie che le diverse componenti del sistema interagiscano correttamente, senza violare le proprietà desiderate.
D'altra parte autorevoli enti, come il CERT della Carnegie Mellon University, riportano un numero sempre crescente di segnalazioni relative alla vulnerabilità dei sistemi informatici, spesso dovute a problemi nella progettazione e realizzazione del software. La soluzione tipica è quella di riparare tali "falle" rendendone più difficile l'utilizzo da parte degli attaccanti, ma questo approccio non va certamente alla radice del problema. Un approccio complementare è, invece, quello di modellare e verificare i requisiti di sicurezza fin dalla specifica di un sistema software, al fine di ridurre al minimo le vulnerabilità sul prodotto finale. L'adozione di tecniche formali può quindi giocare un ruolo molto importante per individuare possibili problemi di sicurezza fin dalle prime fasi di sviluppo, per capirne a fondo le cause e per rimuoverli prima che altre scelte progettuali ci costringano a "inventare" rimedi a posteriori, non sempre possibili e soddisfacenti. L'interesse nei metodi formali per la sicurezza è comprovato da una comunità internazionale sempre più attiva, e dal numero crescente di nuovi workshop e convegni internazionali su tale tema.
Lo scopo di questo progetto è di creare un consorzio formato da 3 Università già attive nella ricerca su metodi formali per la sicurezza e su tecniche per la verifica di proprietà di programmi e protocolli, e focalizzare le proprie energie su obiettivi comuni di ricerca. Si intende operare a largo spettro su diverse problematiche di sicurezza, focalizzando principalmente l'attenzione su tecniche di verifica statiche a livello di linguaggio, che permettano di comprendere e verificare la sicurezza a partire dalla specifica formale di un programma, senza la necessità di analizzarne l'esecuzione. Riteniamo, infatti, che questo approccio sia particolarmente promettente, sia perché si presta ad essere automatizzato tramite algoritmi di verifica efficienti sia per la migliore comprensione degli obiettivi e dei meccanismi di sicurezza che esso fornisce sia a livello di specifica che di programmazione. Ci occuperemo sia di proprietà di alto livello (o livello applicazione), come il controllo dei flussi di informazione e la sicurezza nel "Service-Oriented Computing", sia di proprietà di livello più basso (o livello comunicazione), come l'autenticazione, la segretezza e la non-ripudiabilità su reti di calcolatori e su reti ad-hoc. Considereremo sia modelli simbolici "standard" che modelli computazionali e causali, che ci permetteranno, rispettivamente, di modellare più concretamente aspetti crittografici e di formalizzare proprietà di sicurezza in termini di relazioni esplicite causa-effetto.
Come illustrato in dettaglio nelle sezioni seguenti (si vedano, in particolare, le sezioni 13 sulla descrizione del lavoro e 15 sui risultati attesi), il nostro progetto è di natura fondazionale, visto che si concentra sulla definizione e sullo sviluppo di metodologie formali per l'analisi di diversi aspetti della sicurezza informatica. Quando possibile, comunque, dimostreremo la valenza dei nostri risultati tramite concreti casi di studio provenienti da applicazioni pratiche. <<<

Coordinatore Scientifico del Programma di Ricerca

Riccardo Focardi Università "Ca' Foscari" di VENEZIA

Obiettivo del Programma di Ricerca

La sicurezza dell'informazione è un tema sempre più attuale e rilevante, dato il crescente utilizzo di elaboratori e di reti per applicazioni critiche quali il commercio elettronico, l'home banking, l'acquisto di beni digitali e la fruizione, in genere, di servizi in linea. Diventa quindi sempre più importante capire a fondo i requisiti di sicurezza delle attuali applicazioni distribuite, e studiare metodi per la verifica automatica di tali requisiti.
Lo scopo principale del progetto SOFT è lo studio dei fondamenti della sicurezza informatica e lo sviluppo di metodi formali per la specifica e verifica di proprietà di sicurezza di programmi, sistemi e reti di elaboratori. SOFT comprende 3 Università con 11 ricercatori permanenti, 10 tra dottorandi, assegnisti e post-doc, 2 ricercatori di un ateneo estero e 2 contratti di 6-8 mesi specificatamente richiesti sul programma di ricerca, per un totale di 25 ricercatori. Le unità di ricerca sono caratterizzate da forti competenze su metodi formali per la sicurezza, analisi statica, interpretazione astratta, verifica di proprietà di programmi e semantica della concorrenza. La presenza, inoltre, di due ricercatori della Saarland University di Saarbrücken, e di un dottorando in co-tutela con la Ecole Polytechnique di Palaiseau dimostrano un'apertura verso importanti gruppi di ricerca europei nel settore.
Intendiamo operare a largo spettro su diverse problematiche di sicurezza lavorando sia su proprietà di alto livello (o livello applicazione), come il controllo dei flussi di informazione e la sicurezza nel "Service-Oriented Computing", sia su proprietà di livello più basso (o livello comunicazione), come l'autenticazione, la segretezza e la non-ripudiabilità su reti di calcolatori e su reti ad-hoc. Per quanto riguarda i metodi formali utilizzati, ci concentreremo principalmente su tecniche statiche a livello di linguaggio, che permettano di comprendere e verificare la sicurezza a partire dalla specifica o dal codice di un programma, senza la necessità di analizzarne l'esecuzione. Riteniamo, infatti, che questo approccio sia particolarmente promettente, sia perché si presta ad essere automatizzato tramite algoritmi di verifica efficienti sia per la migliore comprensione degli obiettivi e dei meccanismi di sicurezza che esso fornisce già a livello di specifica o di programmazione.

Il programma di ricerca è suddiviso in fasi e work-package. I work-package si riferiscono a obiettivi specifici del progetto e saranno descritti più avanti. Le fasi, invece, scandiscono il flusso logico e temporale delle attività e corrispondono ad una "agenda standard" nello sviluppo di metodi formali per la sicurezza:

Fase 1 - Linguaggi e modelli per la sicurezza.
Si studieranno linguaggi e modelli orientati alla sicurezza, in cui sia possibile definire e verificare politiche e proprietà per la sicurezza dell'informazione.

Fase 2 - Proprietà di sicurezza.
Si studieranno e si formalizzano proprietà di sicurezza sui linguaggi e modelli definiti durante la fase precedente.

Fase 3 - Tecniche di analisi.
Si studieranno tecniche di analisi per le proprietà e i linguaggi sopra descritti. Tali tecniche saranno principalmente statiche. Si intende, inoltre, implementare ed estendere tool di analisi basati sulle tecniche sopra menzionate.

Ogni work-package interesserà una o più fasi, a seconda della base di partenza e dello stato della ricerca.

WP1 - Sicurezza delle Reti di Comunicazione. Siamo interessati all'analisi di protocolli crittografici tramite interpretazione astratta, sistemi di tipi, control-flow analysis e semantiche causali (vedi anche WP4). Vogliamo estendere lo studio di protocolli crittografici ad applicazioni distribuite basate su crittografia, integrandolo opportunamente con le tecniche di analisi dei programmi studiate in WP2. Svilupperemo nuovi linguaggi e calcoli di processi per la descrizione di sistemi distribuiti che permettano di ragionare su aspetti di sicurezza. Svilupperemo una logica per formalizzare proprietà locali e globali di sistemi distribuiti. Ci interesseremo, infine, di modelli per la sicurezza in reti ad-hoc.

WP2 - Sicurezza a Livello Applicazione. Studieremo diversi aspetti di sicurezza di programmi tramite interpretazione astratta: in particolare, siamo interessati a problemi di verifica di non-interferenza in presenza di attaccanti attivi e su sistemi di calcolo probabilistici; ci occuperemo di confidenzialità e, in particolare, dei "covert channel" noti come "termination channel", in cui l'attaccante ottiene informazioni osservando la terminazione del programma, e di "timing channel" (vedi anche WP3). Studieremo proprietà relative al raffinamento sicuro di programmi che permettano di ottenere uno sviluppo passo-passo di applicazioni sicure a partire da specifiche astratte. Ci interesseremo, infine, dello studio di primitive per la composizione sicura di clienti e servizi nell'ambito del "Service-Oriented Computing".

WP3 - Aspetti Quantitativi della Sicurezza. Intendiamo studiare come alcune delle proprietà affrontate in WP1 e WP2 scalino su modelli più "fini", in cui tempo e probabilità vengono esplicitamente considerati. Studieremo tecniche per individuare e rimuovere attacchi basati sul tempo, trasformando il programma in modo da preservare il comportamento di input/output originale ma modificandone la temporizzazione. Intendiamo, inoltre, sviluppare nuove tecniche di analisi per la sicurezza computazionale di protocolli crittografici. Da un lato studieremo tecniche basate su tipi ed effetti per la correttezza di protocolli basati sulla libreria per operazioni crittografiche di Backes-Pfitzmann-Waidner, dall'altro approfondiremo lo studio della correttezza dell’approccio simbolico rispetto all’approccio computazionale utilizzando le relazioni di simulazione approssimate di Segala e Turrini. Infine, laddove il modello formale si rivela inadeguato a catturare aspetti piu' concreti e legati alla implementazione, vorremmo riuscire ad adattare in modo controllato il modello affiche' possa invece farlo. Cercheremo quindi di avvicinarci agli aspetti solitamente trattati nell'approccio computazionale, senza lasciare la prospettiva formale.

WP4 - Modelli Causali per la Sicurezza. La formalizzazione di varie proprietà di sicurezza può trarre beneficio dal ragionare in termini di causalità tra eventi. Nell'autenticazione tra entità, ad esempio, l'autenticazione da parte del verificatore dovrebbe essere causata dall'esecuzione del protocollo da parte del dichiarante. Intendiamo dare una nuova semantica causale ai protocolli crittografici che permetta di osservare direttamente la relazione di causa ed effetto tra la conclusione del protocollo, e quindi l'autenticazione, e la corrispettiva esecuzione del protocollo da parte dell'entità da autenticare. Intendiamo considerare sia modelli true concurrent come le event structure, sia modelli basati su Proved Transition Systems. <<<

Risultati parziali attesi

Indichiamo, nel seguito, i principali risultati attesi per ogni work-package. Tali risultati sono volutamente molto specifici in modo da poter essere verificati, e costituiranno, quindi, lo strumento primario per la valutazione dell'avvenuto raggiungimento degli obiettivi del progetto. L'interesse per l'avanzamento della conoscenza è stato illustrato in modo estensivo nelle sezioni 12 e 13.

Risultati attesi WP1

Fase 1
- nuovi modelli formali per il trust nelle reti ad-hoc ed integrazione di tali modelli in calcoli di processi.
Fase 2
- una nuova logica temporale per esprimere proprietà di sicurezza di agenti comunicanti.
Fase 3
- definizione di un'interpretazione astratta di protocolli di autenticazione sfida-risposta;
- definizione di nuove analisi control-flow per protocolli di sicurezza;
- estensione del tool presentato in [BBDNN05] alle nuove analisi control-flow;
- utilizzo di tecniche simboliche e di raffinamento per la verifica di proprietà di sicurezza;
- estensione di AVISPA alla logica descritta in fase 2;
- studio di altre possibili estensioni di AVISPA a tecniche sviluppate in questo WP.


Risultati attesi WP2

Fase 1
- definizione di linguaggi imperativi orientati alla sicurezza con primitive di comunicazione crittografiche;
- nuove primitive astratte di comunicazione che permettano di rendere la programmazione indipendente dalla realizzazione crittografica.
Fase 2
- definizione di un framework generale per il raffinamento sicuro di programmi;
- nuove formalizzazioni di proprietà di sicurezza sui calcoli definiti nella fase 1.
Fase 3
- definizione di sistemi di tipi dinamici per la sicurezza di applicazioni distribuite con crittografia;
- estensioni a proprietà nuove e ad aspetti non-funzionali del meccanismo di chiamata per proprietà nel Service-Oriented Computing;
- estensione di tecniche di orchestrazione esistenti a scenari in cui i servizi possono essere pubblicati dinamicamente o diventare non disponibili;
- estensione della non-interferenza astratta ad attaccanti attivi e su sistemi di calcolo probabilistici;
- applicazione della non-interferenza astratta alle basi di dati e al data mining.


Risultati attesi WP3

Fase 1
- nuovo calcolo per protocolli crittografici con semantica simbolica e computazionale basata sulla libreria crittografica di Backes, Pfitzmann e Waidner [BPW03];
- nuovo modello ibrido per protocolli crittografici, in grado di combinare gli approcci simbolico e computazionale;
- estensione dell'algebra di processi LySa per la rappresentazione formale di attacchi basati sulla confusione di tipo.
Fase 2
- nuove formalizzazioni di proprietà di sicurezza sui calcoli definiti nella fase 1.
Fase 3
- sistemi di tipo per protocolli crittografici con semantica simbolica e computazionale.


Risultati attesi WP4

Fase 1
- nuove semantiche causali per calcoli noti di protocolli.
Fase 2
- nuove formalizzazioni di proprietà di sicurezza in stile causale;
- nuove formalizzazioni di proprietà di sicurezza tramite la DSTL.
Fase 3
- specializzazione di tecniche precedentemente studiate sulle nuove semantiche, con particolare attenzione ai protocolli di autenticazione. <<<

Durata

24 mesi

Base di partenza scientifica nazionale o internazionale

Il progetto SOFT si occuperà di diverse tematiche relative ai metodi formali per la sicurezza che introduciamo, nel seguito, menzionando per ognuna di esse i principali risultati presenti in letteratura. Per facilitare la connessione con gli obiettivi del progetto, le tematiche sono state raggruppate in base all'attinenza con i quattro work-package.

- Sicurezza delle Reti di Comunicazione

I protocolli crittografici sono uno degli strumenti fondamentali per garantire sicurezza sulle reti di elaboratori. Nel momento in cui la rete di comunicazione è di grandi dimensioni, e quindi non controllabile localmente, risulta infatti necessario proteggere le informazioni in transito sulla rete tramite tecniche crittografiche. Nonostante le ridottissime dimensioni del codice, tali protocolli sono spesso soggetti ad attacchi in grado di sovvertire la logica del protocollo invalidandone le proprietà di sicurezza attese, senza necessariamente attaccare i sottostanti meccanismi crittografici. Esiste una sconfinata letteratura sull'analisi e verifica di protocolli crittografici, ma solo un piccolo sottoinsieme di tali lavori è basato sull'analisi statica (language-based). In [A99,AB05], ad esempio, viene studiata la segretezza dell'informazione e in [BBDNN05, BFM07, GJ04] l'autenticazione tramite sistemi di tipi e analisi control-flow. Intendiamo approfondire lo studio di tali tecniche focalizzando l'attenzione sull'interpretazione astratta e sulla control flow analysis di protocolli crittografici e lo studio di primitive astratte di comunicazione che permettano di rendere la programmazione indipendente dalla realizzazione crittografica. Inoltre, ci proponiamo di estendere l’analisi simbolica dei protocolli [AVISPA,Bla01,RSGLR00] in modo da consentire la specifica e verifica di una classe più ampia di protocolli e loro proprietà rispetto a quelli attualmente considerati, nonché di diversi modelli di attacco, estendendo lavori esplorativi quali [HDMV05,HDMVB06].
Ci interesseremo, infine, della sicurezza su reti "Ad-hoc". Una rete ad-hoc mobile e' un sistema autonomo costituito da dispositivi che comunicano tra di loro via radio e che sono liberi di muoversi arbitrariamente e in maniera imprevedibile. La nozione di trust in reti ad-hoc è un'area nuova e stimolante [Gli04,PM06] a causa dell'assenza di una infrastruttua di rete fissa, della mobilita' dei nodi, del limitato raggio d'azione della trasmissione, della condivisione del medium, e della vulnerabilità fisica dei dispositivi. Vorremmo sviluppare modelli formali per il trust nelle reti ad-hoc e integrare questi modelli in un calcolo di processi per reti ad-hoc [NH06,Mer07,God07] sviluppando una teoria appropriata per provare formalmente proprietà di sicurezza.

- Sicurezza a Livello Applicazione

Il controllo dei flussi di informazione nei programmi e nei sistemi è un tema piuttosto studiato nell'ambito della teoria della sicurezza. Lo scopo è il controllo delle informazioni denominate "segrete", onde evitare che esse fluiscano verso livelli di utenza non privilegiati e quindi non autorizzati all'accesso delle informazioni stesse. La Non-Interferenza è una delle proprietà di riferimento per realizzare questo tipo di controllo e fu introdotta da Goguen e Meseguer in [GM82]. Essa richiede che la modifica dei dati di alto livello non abbia alcun effetto osservabile a livello più basso o, in altre parole, non interferisca con i livelli inferiori. Esistono moltissime varianti ed estensioni della Non-Interferenza su process calculi e su semplici linguaggi imperativi. Si veda, ad esempio, [BCF02, BCFLP04, FG95, FRS05, GM04, MSZ06, RWW96, RS01, SS00, SM03, SV98]. Focalizzeremo la nostra attenzione sullo studio di Information Flow security in applicazioni distribuite con crittografia, sul raffinamento sicuro di programmi, sulla sicurezza in (frammenti multithreaded di) Java, sull'estensione della non-interferenza astratta [GM04] ad attaccanti più potenti.
La sicurezza risulta cruciale anche nell'ambito del "Service Oriented Computing", in cui le applicazioni si ottengono assemblando componenti, i servizi appunto, distribuiti lungo la rete. I servizi sono aperti, ovvero l'ambiente operativo, i clienti e gli ulteriori servizi non sono completamente specificati. Da qui la necessità di ricorrere ad appositi meccanismi per ottenerne la composizione e coordinazione sicura. I Web Services [S02], basati su tecnologie XML, sono l'esempio più significativo e meglio sviluppato di questo paradigma. Intendiamo estendere i risultati di [BDF06a, BDF06b], in cui si introduce un approccio basato su descrizioni semantiche e una metodologia che rende automatico il processo di scoperta di servizi e la pianificazione della loro composizione sicura. Ci proponiamo inoltre di estendere i modelli e le tecniche sviluppati per i protocolli crittografici ai servizi per la sicurezza. Esistono diversi approcci preliminari [BMPV06,SAMOA] ma nessuno ha raggiunto la maturità necessaria.

- Aspetti Quantitativi della Sicurezza

Recentemente, sono state studiate tecniche che permettono, lavorando a livello di analisi formale, di ottenere risultati anche su modelli computazionali, modelli in cui la sicurezza è definita in termini più classici come resistenza ad un qualsiasi attacco probabilistic polynomial-time, senza quindi considerare la crittografia come inattaccabile (si veda ad esempio [AR00, BCK05, BPW03, L05]). L'analisi formale simbolica descritta fino ad ora permette analisi più semplici e automatizzabili rispetto ai modelli computazionali, e risulta quindi interessante capire se i risultati simbolici scalano sui modelli computazionali, e sotto quali assunzioni crittografiche questo avviene. L'approccio language-based, anche in questo caso, non è stato ancora indagato approfonditamente. Un interessante articolo in questa direzione è [L05] in cui viene proposto un sistema di tipi per la segretezza dei messaggi e, tramite una semantica basata sulla "simulatable cryptographic library" [BPW03], si ottiene la scalabilità dei risultati dal modello simbolico a quello computazionale. Intendiamo sviluppare un'analisi statica basata su [BFM07] per verificare autenticazione su protocolli che usano la "simulatable cryptographic library".
Intendiamo inoltre considerare modelli ibridi che combinino i due approcci: simbolico e computazionale. Esiste già una letteratura in merito [PW01,CCKLLPS06,MRST06,CP07] dalla quale emerge anche un ruolo fondamentale del non determinismo, la cui risoluzione arbitraria può portare a conclusioni indesiderate. I problemi da risolvere sono dunque la gestione del non determinismo e lo studio di tecniche di analisi gerarchica che tengano conto di aspetti computazionali. Un recente caso di studio [ST07] ha analizzato un noto protocollo di autenticazione utilizzando i Probabilistic Automata e una nuova nozione di computationally bounded approximated simulation, che permette al sistema astratto di simulare passi di computazione a meno di un errore trascurabile. Il lavoro costituisce un valido punto di partenza per lo studio di verifica composizionale gerarchica della sicurezza.

- Modelli Causali per la Sicurezza

Nell'ambito dello studio di protocolli crittografici, sono state proposte tecniche in cui le dipendenze causali tra eventi giocano un ruolo estremamente importante [BCM07,CW01,FHG98,P99]. Ne sono esempi gli strand spaces [FHG98] in cui le dipendenze causali sono rese esplicite, e il metodo induttivo di Paulson [P99] in cui le dipendenze sono conseguenza di regole induttive. I Proved Transition Systems [DP92,DP99] sono modelli capaci di catturare la causalità. Li possiamo immaginare come una sorta di rappresentazione compatta delle computazioni, in grado di contenere tutta l’informazione rilevante che si può codificare. Le transizioni sono decorate con etichette che codificano le dimostrazioni, ovvero i passi necessari nella deduzione dell’azione appena eseguita. Ispezionando tali etichette è possible inferire le dipendenze causali, rappresentate con un insieme di riferimenti alle transizioni precedenti. Utilizzando come punto di partenza la semantica arricchita in [BetAl05], intendiamo approfondire lo studio delle semantiche causali basate su Proved Transision Systems e su modelli true-concurrent per l'analisi di protocolli crittografici.
La Distributed State Temporal Logic (DSTL) [MSS04] permette di mettere in relazione causale proprietà che valgono in componenti distinte di un sistema. La logica include un operatore primitivo per specificare eventi, rendendo possibile mescolare condizioni ed eventi nelle formule che definiscono la specifica del sistema. La capacità di usere esplicitamente gli eventi aumenta la capacità espressiva e la semplicità delle specifiche logiche, e sembra essere particolarmente adeguata per descrivere proprietà di sicurezza. Partendo da [MS04], intendiamo indagare ed estendere l'utilizzo della DSTL per specificare e verificare applicazioni in cui le componenti presentano requisiti di sicurezza.


Bibliografia

[A99] M. Abadi. Secrecy by Typing in Security Protocols. Journal of the ACM, 46(5):749–786, 1999.

[AB05] M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. Journal of the ACM, 52(1):102–146, 2005

[AR00] M. Abadi and P. Rogaway. Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption). In proc. of IFIP TCS 2000 (LNCS 1872) pp. 3–22.

[AVISPA] The AVISPA Project. www.avispa-project.org

[BBDNN05] C.Bodei, M.Buchholtz, P.Degano, F.Nielson, H.R.Nielson. Static Validation of Security Protocols. JCS 13(3), 2005.

[BCF02] C.Braghin, A. Cortesi, and R. Focardi. Security Boundaries in Mobile Ambients. Computer Languages, 28(1):101-127, 2002

[BCFLP04] C. Braghin, A. Cortesi, R. Focardi, F.L. Luccio, and C. Piazza. Nesting Analysis of Mobile Ambients. Computer Languages, Systems &amp; Structures 30(3-4):207-230, 2004

[BCK05] M. Baudet, V. Cortier and S. Kremer. Computationally Sound Implementations of Equational Theories against Passive Adversaries, In Proc. of ICALP'05. LNCS 3580. pp. 652-663.

[BCM07] M. Backes, A. Cortesi, M. Maffei. Abstracting Multiplicity in Cryptographic Protocols. In Proc. of IEEE CSF'07, pp. 355-369

[BDF06a] M.Bartoletti, P.Degano, G.L.Ferrari. Plans for service composition. Proc. of WITS, 2006.

[BDF06b] M.Bartoletti, P.Degano. G.L.Ferrari. Types and effects for secure orchestration. Proc. of IEEE CSFW, 2006.

[BetAl5] C.Bodei, M.Buchholtz, P.Degano, M.Curti, C.Priami, F.Nielson, H.R.Nielson. On Evaluating the Performance of Security Protocols specified in Lysa. Proc. of PACT05, LNCS 3606.

[BFM07] M. Bugliesi, R. Focardi and M. Maffei. Dynamic Types for Authentication, Journal of Computer Security, IOS Press, 15(6):563-617, 2007

[Bla01] B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. IEEE CSFW’01

[BMPV06] M. Backes, S. Moedersheim, B. Pfitzmann, L. Vigano`. Symbolic and Cryptographic Analysis of the Secure WS-Reliable Messaging Scenario. In Proc. of FOSSACS’06. LNCS 3921.

[BPW03] M. Backes, B. Pfitzmann, and M. Waidner. A Universally Composable Cryptographic Library. In proc. of ACM CCS 2003, pp. 220-230.

[CCKLLPS06] R. Canetti, L. Cheung, D. Kirli Kaynar, M. Liskov, N. A. Lynch, O. Pereira, R. Segala: Time-Bounded Task-PIOAs: A Framework for Analyzing Security Protocols. In Proc. of DISC’06. LNCS 4167, pp 238-253.

[CP07] K. Chatzikokolakis, C. Palamidessi. Making Random Choices Invisible to the Scheduler. In Proc. of CONCUR’07. LNCS 4703, pp. 42-58.

[CW01] F.Crazzolara, G.Winskel. Events in Security Protocols. In ACM CCS, 2001.

[DP92] P.Degano, C.Priami. Proved Trees. In Proc. of ICALP'92.

[DP99] P.Degano, C.Priami. Non Interleaving Semantics for Mobile Processes. TCS 216, 1999.

[FG95] R. Focardi and R. Gorrieri, A Classification of Security Properties for Process Algebras, Journal of Computer Security, 3(1):5-33, 1995

[FHG98] F.J.T. Fábrega, J.C.Herzog, J.D.Guttman. Strand spaces: Why is a security protocol correct? JCS 7(2-3), 1999.

[FRS05] R. Focardi, S. Rossi, A. Sabelfeld: Bridging Language-Based and Process Calculi Security. In Proc. of FoSSaCS 2005 pp. 299-315. LNCS 3441

[GJ04] A. D. Gordon and A. Jeffrey. Types and effects for asymmetric cryptographic protocols. Journal of Computer Security, 12(3-4):435–483, 2004

[Gli04] V.D.Gligor. Security of Emergent Properties in Ad-Hoc Networks. Security Protocols Workshop 2004

[GM04] R. Giacobazzi and I. Mastroeni. Abstract Non-Interference. POPL'04

[God07] J.C. Godskesen. A Calculus for Mobile Ad Hoc Networks. COORDINATION'07

[HDMV05] P. Hankes Drielsma, S. Moedersheim, L. Vigano`. A Formalization of Off-Line Guessing for Security Protocol Analysis. LPAR04

[HDMVB06] P. Hankes Drielsma, S. Moedersheim, L. Vigano`, D. Basin. Formalizing and Analyzing Sender Invariance. FAST’06

[L05] P. Laud. Secrecy types for a simulatable cryptographic library. In Proc. of the 12th ACM CCS '05. New York, NY, 26-35.

[MRST06] J. C. Mitchell, A. Ramanathan, A. Scedrov, V. Teague. A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. TCS 353, 2006

[MSZ06] A. C. Myers, A. Sabelfeld, and S. Zdancewic. Enforcing Robust Declassification. Journal of Computer Security, 14(2):157-196, 2006.

[NH06] S.Nanz, C.Hankin. A Framework for Security Analysis of Mobile Wireless Networks. TCS 367, 2006

[Mer07] M.Merro. On the Observational Theory of Mobile Ad-Hoc Networks. Information and Computation, to appear.

[MSS04] C.Montangero, L. Semini and S. Semprini. Logic Based Coordination for Event-Driven Self-Healing Distributed Systems. Proc. of COORDINATION'04, LNCS 2949.

[MS04] C.Montangero, L. Semini. Formalizing an Adaptive Security Infrastructure in Mobadtl. Proc. of FCS'04.

[P99] L.C.Paulson. Proving security protocol correct. Proc. of Lics, 1999.

[PM06] A.A. Pirzada, C.McDonald. Trust Establishment in Pure Ad-Hoc Networks. Wireless Personal Communication 379, 2006

[PW01] B. Pfitzmann, M. Waidner: A Model for Asynchronous Reactive Systems and its Application to Secure Message Transmission. IEEE Symposium on S&amp;P 2001

[RS01] P. Ryan and S. Schneider, Process algebra and Non-Interference, Journal of Computer Security 9(1/2):75–103, 2001.

[RSGLR00] P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and B. Roscoe. Modelling and Analysis of Security Protocols. 2000

[RWW96] A.W. Roscoe, J.C.P. Woodcock and L. Wulf, Non-Interference through determinism, Journal of Computer Security 4(1):27-54, 1996.

[S02] M.Stal. Web services: Beyond component-based computing. Comms. Of the ACM 55(10), 2002.

[SAMOA] Samoa: Formal Tools for Securing Web Services. http://research.microsoft.com/projects/samoa/.

[SS00] A. Sabelfed and D. Sands, Probabilistic Noninterference for multi-threaded programs, in: Proc. of IEEE CSFW 2000, pp.200-215.

[SM03] A. Sabelfeld and A.C. Myers, Language-based information-flow security, IEEE Journal on Selected Areas in Communication 21(1):5-19, 2003.

[ST07] R. Segala, A. Turrini. Approximated Computationally Bounded Simulation Relations for Probabilistic Automata. IEEE CSF07

[SV98] G. Smith and D.M. Volpano, Secure information flow in a multi-threaded imperative language, in: Proc. of 25th ACM POPL, pp.355-364, 1998 <<<