Automatic Verification of Internet Security protocols

FIRB - Security DIT-PRJ-03-011

Status NOT active project
DISI role Partner
Project type Research Project
Dimension National
Acquisition date 2004-01-20
Start date 2004-01-20
End date 2007-01-19
SAP code 40100704

Project details

Project astract Our economic, political, and social life today depends vitally on communication and IT infrastructures, in particular the Internet. The acceptance and continued expansion of these infrastructures depends on trust: all participants must have confidence in their security, which is integrated into the infrastructure either by means of specific security protocols or protocol families (cf. protocols like IPSec, IKE, TLS, and SSH). In open networks protocols should work even under worstcase assumptions, e.g. messages may be eavesdropped or tampered with by an "intruder" or careless principals. Severe attacks can be conducted even without breaking cryptography, but by exploiting weaknesses in the protocols themselves. These attacks oftem stems from subtle misconceptions in the design of the protocols which are very difficult for humans to determine, due to the complex ways different protocol sessions could be interleaved, and the possible interferences of malicious intruders.<br/><br/>The overall goals of the project are:<br/>* to develop a rich specification language for formalizing protocols, security goals, and threat models for protocols of industrial complexity, building upon existing standards for protocol specification (e.g. SDL, ASN.1, UML-CD, etc.)<br/>* to advance the stateoftheart modelchecking techniques to scale up to this complexity,<br/>* to build a platform based on these techniques that will allow industry and standardization experts to automatically validate or detect errors, and<br/>* to tune the tool composing this platform and demonstrate proofofconcept on a large collection of practically relevant, Internet protocols.<br/><br/>The partners have previously carried out extensive work that lays the foundations of the proposed technology. They have developed independently a number of different verification and validation techniques based on<br/>* (i) finite-state analysis by reduction to propositional satisfiability checking,<br/>* (ii) infinite-state verification based on interactive theorem-proving,<br/>* (iii) model checking interactive distributed systems based on process algebras,<br/>* (iv) on model-checking of multi-agent finite state machines.<br/><br/>The techniques developed by the partners exhibit a strong form of complementarity. On the one hand, (i) and (iv) cope with the infinity of the search space by building and analyzing approximations of the problem which are then iteratively improved. These techniques are thus most suited for error detection: while (i) has proved very effective in finding attacks carried out by an active intruder, (iv) can identify flaws by showing that protocols do not ensure the expected security goals. On the other hand, (iii) aims at establishing the equivalence between a model known to enjoy the desired security property and the actual model and therefore­- together with (ii)­-is suited for verification.<br/><br/>The effectiveness of the approaches on small and medium size protocols has been demonstrated in previous work. However, whether the approaches scaleup to the new generation of largescale, security protocols remains a challenge. This will leads us to<br/>* investigate methods for specifying largescale protocols, security properties and goals as well as models of intruders and threats;<br/>* improve and integrate the verification and model-checking techniques previously<br/>developed by the partners to scale up to industrial security protocols;<br/><br/>This will be done (i) by developing an integrated verification platform based on them, (ii) by selecting a set of securitysensitive Internet protocols, and (iii) by using the tools to automatically analyze the selected protocols.
Fundings 300000 €
Partners
  • DIST - Università di Genova
  • Università di Napoli "Federico II"
  • DIT - University of Trento
  • DIST - Universit
  • Universit

DISI Sub-project details

Project astract Il DIT dell'Univesità di Trento (UNITN) ha un'elevata visibilità internazionale nell'ambito delle tecnologie di soddisfacibilità ragionamento automatico e model checking con automi nell'ambito della verifica di hardware e software e nella verifica della sicurezza. Il compito dell'unità di ricerca di UNITN si articolerà nelle seguenti attività:<br/>Analisi, insieme ad UNIGE ed UNINA, dei linguaggi di specifica per protocolli di sicurezza disponibili in letteratura e adattamento di un linguaggio di specifica adeguato per gli scopi del presente progetto. Sviluppo e/o adattamento del traduttore dal linguaggio di specifica selezionato al formato comune agli strumenti di analisi sviluppati.<br/>Sviluppo ed ottimizzazione di tecniche di model-checking per protocolli di sicurezza basati su automi estesi. In particolare si prevede lo sviluppo di tecniche di HD-automi e tecniche di ragionamento basato su astrazione iterativa per HD-automi che si appoggi su tecniche di model-checking tradizionale. Ciò richiederà lo svolgimento di attività di ricerca sia nell'ambito dello sviluppo di tecniche di codifica dei problemi di sicurezza in formalismi e/o procedure basati su HD-automi e/o logiche corrispondenti, sia lo sviluppo di sistemi per l'analisi di automi estesi (con vincoli e nomi) allo stato dell'arte (ad es. HD-automi, simmetrie e broadcast, vincoli aritmetici).<br/>Selezione e formalizzazione di problemi di sicurezza tratti da protocolli di sicurezza di ultima generazione, con particolare riferimento ai nuovi requisiti di tali protocolli (mobilità tamper resistance etc.). Per lo svolgimento di tale attività sono previste collaborazioni con Centri di Ricerca e Industrie attive nel settore e discussione con gli organismi di standardizzazione quali, ad esempio, l'IETF.<br/>Collaborazione scientifica all'organizzazione da parte di UNIGE di un workshop internazionale sull'analisi automatica di protolli di sicurezza e sulla specifica dei requisiti.
Fundings 96000 €
Manager Fabio Massacci