This thesis documents a framework for verifying secrecy and authenticity properties of Mobile Ad-hoc Networks. We present the Distributed Applied Pi Calculus with Broadcast, which is a simple, yet generic, expressive, and lightweight extension to the well-established Applied Pi calculus consisting of connectivity graphs, broadcast primitives, and explicit locations. The calculus can be instantiated by an arbitrary Term Rewrite System, and the semantics of the calculus is largely like that of Applied Pi. We inherit key definitions of secrecy and authenticity from Applied Pi to our calculus, as well as those of frames and static equivalence. We prove a powerful teorem expressing a syntactic relationship between Horn clauses generated from a process in the calculus of Abadi and Blanchet, and the source process. Several interesting corollaries follow from this theorem, including that Horn clause deduction overapproximates active syntactic secrecy, and that claims of message-passing deduced from the Horn clauses are sound with regards to the messages passed in the source process. During the process of this proof, we observe a frequently overlooked assumption in the Dolev-Yao threat model which causes frames to become inconsistent if particular internal reductions are performed. To address this, we give a (easily generalised) revelation semantics which ensures frames are consistent in the presense of such reductions. At last, specifying how to extend the Horn clause generator to take into account connectivity graphs, We inherit a proof of soundness of deduction from Horn clauses for our calculus, thus clearing the way for the application of automated Horn clause constraint solvers.