The Ad-hoc On-demand Distance Vector (AODV) routing protocol is a routing protocol used for dynamic wireless networks where nodes can enter and leave the network at will. To find a route to a particular destination node, the source node broadcasts a RREQ to its immediate neighbors. If one of these neighbors has a route to the destination, then it replies back with a RREP. Otherwise the neighbors in turn rebroadcast the request. This continues until the RREQ hits the final destination or a node with a route to the destination. At that point a chain of RREP messages is sent back and the original source node finally has a route to the destination.
We proved that AODV protocol never produces routing loops by proving that a combination of sequence numbers and hop counts is monotonic along a route. This means that there can't be any loop in the routing table. The proof was done completely automatically and our algorithm was able to generate all the predicates needed.
We didn't model route timeouts (routes can time out after a certain amount of time), since we don't have a suitable method of doing that.
(murphi-program (constant-decls (INVALID 0) (RREQ 1) (RREP 2)) (deftype cell-index-type rat) (deftype msg-index-type rat) (global-state (route-p (array (array bool cell-index-type) cell-index-type)) (route (array (array cell-index-type cell-index-type) cell-index-type)) (hops (array (array rat cell-index-type) cell-index-type)) ;; Message queue (msg-type (array rat msg-index-type)) (msg-src (array cell-index-type msg-index-type)) (msg-dst (array cell-index-type msg-index-type)) (msg-to (array cell-index-type msg-index-type)) (msg-from (array cell-index-type msg-index-type)) (msg-hops (array rat msg-index-type)) ;; Initialization arrays (init-false (array (array bool cell-index-type) cell-index-type)) (init-invalid (array rat msg-index-type)) (init-hops (array (array rat cell-index-type) cell-index-type)) ;; Monitor variables (a cell-index-type) (b cell-index-type) (c cell-index-type)) (axiom (and (not (= a b)) (not (= a c)) (not (= b c)) (forall (x msg-index-type) (and (>= (aref msg-hops x) 0) (= (aref init-invalid x) INVALID))) (forall (x cell-index-type) (forall (y cell-index-type) (and (not (aref (aref init-false x) y)) (= (aref (aref init-hops x) y) 0) (>= (aref (aref hops x) y) 0)))) (forall (x rat) (forall (y rat) (<=> (> x y) (>= x (+ y 1))))))) (initialize (progn (setq msg-type init-invalid) (setq route-p init-false) (setq hops init-hops))) (ruleset ((index-in msg-index-type) (index-out msg-index-type) (cell cell-index-type) (dst cell-index-type)) ;; Map ;; #1= (aref msg-to index-in) ;; #2= (aref msg-from index-in) ;; #3= (aref msg-src index-in) ;; #4= (aref msg-dst index-in) ;; #5= (aref msg-hops index-in) ;; Inject RREQ (==> (and (= (aref msg-type index-out) INVALID) (not (aref (aref route-p cell) dst))) (progn (setq (aref msg-type index-out) RREQ) (setq (aref msg-src index-out) cell) (setq (aref msg-dst index-out) dst) (setq (aref msg-from index-out) cell) (setq (aref msg-hops index-out) 0))) ;; Read RREQ (==> (and (= (aref msg-type index-out) INVALID) (= (aref msg-type index-in) RREQ) (/= #1=(aref msg-to index-in) #2=(aref msg-from index-in)) (/= #3=(aref msg-src index-in) #4=(aref msg-dst index-in)) (/= a c) (/= a b) (/= b c) (/= #2# #4#) (/= #1# #3#) ) (progn ;; Add route to immediate neighbor (setq (aref route-p #1# #2#) true) (setq (aref route #1# #2#) #2#) (setq (aref hops #1# #2#) 1) ;; Add route to sender (ite (or (>= (aref (aref hops #1#) #3#) (+ 1 #5=(aref msg-hops index-in))) (not (aref (aref route-p #1#) #3#))) (progn (setq (aref route-p #1# #3#) true) (setq (aref route #1# #3#) #2#) (setq (aref hops #1# #3#) (+ #5# 1))) (skip)) ;; Reply if we have route, otherwise forward (ite (= #4# #1#) ;; We are the final destination (progn (setq (aref msg-type index-out) RREP) (setq (aref msg-src index-out) #4#) (setq (aref msg-dst index-out) #3#) (setq (aref msg-from index-out) #1#) (setq (aref msg-to index-out) #2#) (setq (aref msg-hops index-out) 0)) (ite (aref (aref route-p #1#) #4#) ;; We have a route to final destination (progn (setq (aref msg-type index-out) RREP) (setq (aref msg-from index-out) #1#) (setq (aref msg-to index-out) #2#) (setq (aref msg-src index-out) #4#) (setq (aref msg-dst index-out) #3#) (setq (aref msg-hops index-out) (aref (aref hops #1#) #4#)) ) ;; Forward RREQ (progn (setq (aref msg-type index-out) RREQ) (setq (aref msg-from index-out) #1#) (setq (aref msg-src index-out) #3#) (setq (aref msg-dst index-out) #4#) (setq (aref msg-hops index-out) (aref (aref hops #1#) #3#))))))) ;; Read RREP (==> (and (= (aref msg-type index-out) INVALID) (= (aref msg-type index-in) RREP) (/= #1# #2#) (/= #3# #4#) (/= a c) (/= a b) (/= b c) (/= #2# #4#) (/= #1# #3#)) (progn ;; Add route to immediate neighbor (setq (aref route-p #1# #2#) true) (setq (aref route #1# #2#) #2#) (setq (aref hops #1# #2#) 1) ;; Add route to sender (ite (or (>= (aref (aref hops #1#) #3#) (+ 1 #5#)) (not (aref (aref route-p #1#) #3#))) (progn (setq (aref route-p #1# #3#) true) (setq (aref route #1# #3#) #2#) (setq (aref hops #1# #3#) (+ #5# 1))) (skip)) (ite (= #4# #1#) ;; We are the final destination (skip) (ite (aref (aref route-p #1#) #4#) ;; We have route to final destination (progn (setq (aref msg-type index-out) RREP) (setq (aref msg-from index-out) #1#) (setq (aref msg-to index-out) (aref (aref route #1#) #4#)) (setq (aref msg-src index-out) #3#) (setq (aref msg-dst index-out) #4#) (setq (aref msg-hops index-out) (aref (aref hops #1#) #3#))) (skip))))) ) (invariant (=> (and (aref (aref route-p a) c) (= (aref (aref route a) c) b)) (and (aref (aref route-p b) c) (> (aref (aref hops a) c) (aref (aref hops b) c))))) (abstraction (B0 (aref (aref route-p a) c)) (B1 (= (aref (aref route a) c) b)) (B2 (aref (aref route-p b) c)) (B3 (> (aref (aref hops a) c) (aref (aref hops b) c))) ;;; Generated predicates... ;; Iteration 1 (C0 (FORALL (X18 msg-index-type) (NOT (= (AREF MSG-TYPE X18) 1)))) ;; Iteration 2 (C6 (FORALL (X22 msg-index-type) (NOT (= (AREF MSG-TYPE X22) 2)))) ;; Iteration 3 (C1 (FORALL (X19 msg-index-type) (NOT (AND (= (AREF MSG-SRC X19) C) (= (AREF MSG-FROM X19) B) (= (AREF MSG-TYPE X19) 1))))) ;; Iteration 4 (C7 (FORALL (X23 msg-index-type) (NOT (AND (= (AREF MSG-SRC X23) C) (= (AREF MSG-FROM X23) B) (= (AREF MSG-TYPE X23) 2))))) ;; Iteration 5 (C2 (FORALL (X24 msg-index-type) (NOT (AND (= (AREF MSG-TYPE X24) 1) (= (AREF MSG-SRC X24) C) (= (AREF MSG-FROM X24) B) (= (+ -1 (* -1 (AREF MSG-HOPS X24)) (* 1 (AREF (AREF HOPS B) C))) 0))))) ;; Iteration 6 (C3 (FORALL (Y24 msg-index-type) (NOT (AND (= (AREF MSG-TYPE Y24) 1) (= (AREF MSG-SRC Y24) C) (= (AREF MSG-FROM Y24) B) (= (AREF MSG-HOPS Y24) 0))))) ;; Iteration 7 (C4 (FORALL (X25 msg-index-type) (NOT (AND (< (+ 1 (* -1 (AREF (AREF HOPS B) C)) (* 1 (AREF MSG-HOPS X25))) 0) (= (AREF MSG-TYPE X25) 1) (= (AREF MSG-FROM X25) B) (= (AREF MSG-SRC X25) C))))) ;; Iteration 8 (C5 (FORALL (X26 msg-index-type) (NOT (AND (= (+ -1 (* -1 (AREF MSG-HOPS X26)) (* 1 (AREF (AREF HOPS B) C))) 0) (= (AREF MSG-FROM X26) B) (= (AREF MSG-SRC X26) C) (= (AREF MSG-TYPE X26) 2))))) ;; Iteration 9 (C8 (FORALL (X24 msg-index-type) (NOT (AND (= (AREF MSG-HOPS X24) 0) (= (AREF MSG-TYPE X24) 2))))) (C9 (< (+ 1 (* -1 (AREF (AREF HOPS B) C))) 0)) ;; Iteration 10 (C10 (= (+ 1 (* -1 (AREF (AREF HOPS A) C))) 0)) (C11 (= (AREF (AREF ROUTE A) C) B)) ;; Iteration 11 (C12 (< (+ 1 (* -1 (AREF (AREF HOPS A) C))) 0)) ;; Iteration 12 (C13 (FORALL (Y30 msg-index-type) (NOT (AND (= (AREF MSG-HOPS Y30) 0) (= (AREF MSG-SRC Y30) C) (= (AREF MSG-FROM Y30) B) (= (+ 2 (* -1 (AREF MSG-TYPE Y30))) 0))))) ;; Iteration 13 (C14 (= (+ 0 (* -1 (AREF (AREF HOPS B) C))) 0)) ;; Iteration 14 (C15 (FORALL (X31 msg-index-type) (NOT (AND (= (AREF MSG-TYPE X31) 2) (= (AREF MSG-FROM X31) B) (= (AREF MSG-SRC X31) C) (< (+ 1 (* 1 (AREF MSG-HOPS X31)) (* -1 (AREF (AREF HOPS B) C))) 0))))) ))