Verification of Correspondence Assertions in a Calculus for Mobile Ad Hoc Networks

Hans Hüttel, Morten Kühnrich, Jens Christian Godskesen

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

Abstrakt

We introduce a novel process calculus called DBSPI (distributed broadcast SPI-calculus) which models mobile ad hoc networks (MANET). The calculus is a cryptographic broadcast calculus with locations and migration. Communication and migration are limited to neighborhoods. Neighborhood definitions are explicitly part of the syntax allowing dynamic extension using bound identifiers. In this semantic setting we study authentication of agents in MANET protocols. A safety property dealing with authentication correspondence assertions is defined. Later a dependent type and effect system is given and it is shown to be sound, i.e. protocols which are typeable are also safe. This result is lifted to open systems which involves Dolev-Yao attackers. Our Dolev-Yao attacker may use public keys for encryption and can attack any neighborhood it wishes. Our technique is applied to the Mobile IP registration protocol – a type check shows it is safe. To our knowledge this is the first type system for a MANET calculus doing that.
OriginalsprogEngelsk
TitelProceedings of the 7th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2008)
Antal sider16
Vol/bind2
ForlagElsevier
Publikationsdato2009
Udgave229
Sider77-93
DOI
StatusUdgivet - 2009
Begivenhed7th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2008) - Reykjavik, Island
Varighed: 13 jul. 200813 jul. 2008
Konferencens nummer: 7

Konference

Konference7th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2008)
Nummer7
LandIsland
ByReykjavik
Periode13/07/200813/07/2008
NavnElectronic Notes in Theoretical Computer Science
Nummer229
Vol/bind2
ISSN1571-0661

Emneord

  • Proceskalkyle
  • Typer
  • Kryptografiske protokoller

Fingeraftryk Dyk ned i forskningsemnerne om 'Verification of Correspondence Assertions in a Calculus for Mobile Ad Hoc Networks'. Sammen danner de et unikt fingeraftryk.

Citationsformater