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.
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.
Originalsprog | Engelsk |
---|---|
Titel | 20th Nordic Workshop on Programming Theory NWPT 2008 |
Antal sider | 3 |
Forlag | Institute of Cybernetics at Tallinn University of Technology |
Publikationsdato | 2008 |
Sider | 54-56 |
ISBN (Elektronisk) | 978-9949-430-24-6 |
Status | Udgivet - 2008 |
Begivenhed | Nordic Workshop on Programming Theory - Tallinn, Estland Varighed: 19 nov. 2008 → 21 dec. 2008 Konferencens nummer: 20 |
Konference
Konference | Nordic Workshop on Programming Theory |
---|---|
Nummer | 20 |
Land/Område | Estland |
By | Tallinn |
Periode | 19/11/2008 → 21/12/2008 |