In previous work, we proposed a “Bootstrap” protocol for establishing neighbor relationships, between two mobile nodes in a mission critical deny-by-default Mobile Ad-hoc Network. In this paper, we formally characterize the security properties of this Bootstrap protocol, striving to answer the following questions: 1) To what extent can an adversary undermine the correctness and performance of the Bootstrap protocol? 2) To what extent can the Bootstrap protocol be improved in anticipation of an adversary? Our analyses employ a combination of formal logic and two standard automated model checkers, SPIN and PRISM. Two types of threats are considered, which we call the subverted node and the subverted link. In the subverted link analysis, we further categorize the adversary into two variants, which we call dark-red or light-red in correspondence with having detailed Bootstrap-protocol-specific knowledge or only generic neighbor setup knowledge, respectively. The subverted node analysis shows that the adversary cannot TCP-SYN-flood-like attack nor deadlock the good node within the Bootstrap protocol. The subverted link analysis shows that the adversary cannot undermine the correctness of the protocol, in the sense that the protocol''s performance is only degraded in a bounded manner by the dark-red adversary or in a benign manner by the light-red adversary.
展开▼
