Bruno Blanchet Equipe Interpretation abstraite

De
Publié par

Action Specifique Securite Bruno Blanchet Equipe Interpretation abstraite sous la direction de Patrick Cousot Departement d'Informatique, Ecole Normale Superieure Mai 2002

  • analyse de protocoles cryptographiques

  • determiner des proprietes semantiques des programmes

  • analyse de processus du pi calcul et des ambients

  • analyse de programmes probabilistes pour la securite

  • equipe interpretation abstraite

  • analyse de confidentialite pour le code mobile

  • instances du meme processus


Publié le : mercredi 1 mai 2002
Lecture(s) : 38
Source : di.ens.fr
Nombre de pages : 31
Voir plus Voir moins
ActionSp´eciqueSe´curit´e
Bruno Blanchet Interpre´tationa
´ EquipeInterpre´tationa bstraite
sous la direction de Patrick Cousot
D´partement d’Informatique, e ´ EcoleNormaleSup´erieure
NormaleSup´erieure
Mai
2002
PartieI:letravaildele´quipeInterpre´tationabstraite duLIENSpourlActionSp´eciqueS´ecurit´e
Analyse de protocoles cryptographiques (David Monniaux, Bruno Blanchet)
Analysedecondentialite´pourlecodemobile (J´eroˆmeF´eret)
Tatouage semantique de logiciel ´ (Patrick Cousot, projet TUAMOTU du RNRT)
S´ecurisationdeprogrammesparcontroˆleurdexe´cution (PatrickCousot,avecRadhiaCousot,´EcolePolytechnique)
Futur :edysroepamgrspmeaborilibsetsruoptie´cerual´snAla (David Monniaux)
1
Analyse de protocoles cryptographiques
Proce´duresdede´cisionpourleslogiques de croyances, comme BAN et GNY (David Monniaux).
Ve´ricationdesecretencalculantunesurapproximationdelensemble desmessagesquelattaquantpeutavoir,repr´esent´eepardes automates d’arbres(David Monniaux).
Repre´sentationabstraitedesprotocolespardes clauses de Horn(Bruno Blanchet)
2
Analysedecondentialit´epourlecodemobile(J´erˆomeFeret)
Analyse de processus dupi calculet desambientspour obtenir une descriptiondescommunicationsdansunsyste`me,etcompterles occurrences de processus.
Peut traiter un nombre
illimit´ed’instances.
Distingueetnere´idestancsinssu.ecsspeormˆemdu
eMliruel´rpesicenoileuenasaselyr´spqcee´edtnse.
Rapide en pratique (moins d’1 s sur beaucoup d’exemples).
3
Tatouagese´mantiquedelogiciel(PatrickCousot)
Tatouage =eld´bi´erqmainueelqui indique l’origine du logiciel (protection contre le piratage).
Ide´e:linterpre´tationabstraitepermetded´eterminerdes proprie´t´ess´emantiquesdesprogrammes
construire un
tat ´ antique. ouage sem
Tatouageinvisible`alex´ecution, maisre´cupe´rablepardesanalyseursabstraits.
Techniquebrevete´eavecThale`s.
4
S´ecurisationdeprogrammesparcontrˆoleurdex´ecution (P. et R. Cousot)
But :Limiter les comportementsd’un programmeP`aceux autorise´sparunesp´ecicationdonn´ee.
Laspe´cicationestexprime´eparunprogrammeM(contreloˆru dexe´cution),quipeutavoirtouslescomportementsautorise´s.
On transformePen un programme qui executer uneaction interditeparM. ´
bloquequand il allait
5
Analyse de programmes probabilistes (David Monniaux)
But : trouver unmajorantdedt´libibaroapel´vnenie´reatucntemen (par exemple une erreur, une panne, ...)
Applicationsa`las´ecurite´,a`explorer:
´Vericationdeprotocoles cryptographiquestenant compte des aspectsprobabilistes.
ledetsiabilprobtionlisadoe´M exemple)
environnement(reseau par ´
6
Part II: Secrecy for cryptographic protocols (Bruno Blanchet)
Introduction
Protocol representation
Solving algorithm
Results and conclusion
7
Example
Denning-Sacco key distribution protocol (simplified)
Message 1.AB:{{k}skA}pkB Message 2.BA:{s}k
The goal of the protocol is to keepssecret.
kfresh
8
The attack
The (well-known) attack against this protocol.
Message 1.AC:{{k}skA}pkC Message 1’.C(A)B:{{k}skA}pkB Message 2.BC(A) :{s}k
The attackerCimpersonatesAand obtains the secrets.
9
Our goal
Goal: a verifier for cryptographic protocols
Fully automatic.
For an
unboundedthe number of sessions of the protocol.
Efficient(no state space explosion).
Example: secrecy properties of Skeme in 17 ms, less than 2 Mb.
10
Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.