Secrecy in Mobile Ad-hoc Networks

Hans Hüttel, Willard Rafnsson

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

Abstract

We propose a framework for automated verification of secrecy properties of
MANET protocols, consisting of a formal language and a proven sound verifi-
cation technique which can be automated. We start off by presenting the dis-
tributed applied pi calculus with broadcast (DAπβ ), whereafter we summarise
our procedure for generating Horn clauses from a DAπβ model expressing con-
trol flow in the model. We then present our soundness result, from which it
follows that the generated Horn clauses can be used to reason about secrecy in
the source model, in an automated manner.
OriginalsprogEngelsk
Titel20th Nordic Workshop on Programming Theory NWPT 2008
Antal sider3
ForlagInstitute of Cybernetics at Tallinn University of Technology
Publikationsdato2008
Sider54-56
ISBN (Elektronisk)978-9949-430-24-6
StatusUdgivet - 2008
BegivenhedNordic Workshop on Programming Theory - Tallinn, Estland
Varighed: 19 nov. 200821 dec. 2008
Konferencens nummer: 20

Konference

KonferenceNordic Workshop on Programming Theory
Nummer20
Land/OmrådeEstland
ByTallinn
Periode19/11/200821/12/2008

Fingeraftryk

Dyk ned i forskningsemnerne om 'Secrecy in Mobile Ad-hoc Networks'. Sammen danner de et unikt fingeraftryk.

Citationsformater