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

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

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of the 7th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2008)
Number of pages16
Volume2
PublisherElsevier
Publication date2009
Edition229
Pages77-93
DOIs
Publication statusPublished - 2009
Event7th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2008) - Reykjavik, Iceland
Duration: 13 Jul 200813 Jul 2008
Conference number: 7

Conference

Conference7th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2008)
Number7
CountryIceland
CityReykjavik
Period13/07/200813/07/2008
SeriesElectronic Notes in Theoretical Computer Science
Number229
Volume2
ISSN1571-0661

    Fingerprint

Keywords

  • Process calculus
  • Types
  • Cryptographic protocols

Cite this

Hüttel, H., Kühnrich, M., & Godskesen, J. C. (2009). Verification of Correspondence Assertions in a Calculus for Mobile Ad Hoc Networks. In Proceedings of the 7th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2008) (229 ed., Vol. 2, pp. 77-93). Elsevier. Electronic Notes in Theoretical Computer Science, No. 229, Vol.. 2 https://doi.org/doi:10.1016/j.entcs.2009.06.030