@conference {
	title = {Modeling vulnerabilities of ad hoc routing protocols},
	author = {Yang, Shahan., Baras, John S.},
	year = {2003},
	month = {12/2003},
	abstract = {The purpose of this work is to automate the analysis of ad hoc routing protocols in the presence of attackers. To this end, a formal model fo protocol behavior is developed in which time is modeled by a set of constraints on the time of occurrence of events, enabling the representation of partially ordered timed events and asynchronous communication. Data variables are represented symbolically, capturing a range of distinct executions in each expression. Given a formal description of Ad Hoc On-Demand Distance Vector Routing Algorithm (AODV) and the desired safety property (route stability), an analysis by a naive semi-decision procedure discovers an instance of an attack that leads to a violation of the property.},
	address = {Fairfax, Virginia},
	booktitle = {1st ACM workshop on Security of ad hoc and sensor networks},
	pages = {pp. 12-20.},
	organization = {George Mason University}
}
@conference {
	title = {Correctness Proof for a Dynamic Adaptive Routing Algorithm for Mobile Ad-hoc Networks},
	author = {Yang, Shahan., Baras, John S.},
	year = {2003},
	month = {07/2003},
	abstract = {Dynamic and adaptive routing algorithms are the {\textquotedblleft}brains{\textquotedblright} of mobile ad-hoc networks (MANETs), in that they govern the self-organization of these networks. MANETs are infrastructureless {\textquotedblleft}intelligent{\textquotedblright} networks, which are becoming increasingly popular and have wide applicability. In this paper, we view dynamic adaptive routing algorithms for MANETs as hybrid systems (partly based on logic and partly based on numerics). In this paper, we introduce formal models for the analysis and verification of one such routing algorithm, the Temporally Oriented Routing Algorithm (TORA) under certain assumptions. More specifically we give a rigorous mathematical proof of correctness and convergence of TORA. Other formal methods, their limitations~and future research challenges are also discussed.},
	address = {Lake Baikal, Russia},
	booktitle = {IFAC Workshop \&ndash; Modeling and Analysis of Logic Controlled Dynamic Systems},
	pages = {pp. 1-10}
}
@conference {
	title = {Finite Automata Models for Anomaly Detection},
	author = {V. R. Ramezani, Yang, Shahan., Baras, John S.},
	year = {2003},
	month = {03/2003},
	abstract = {A fundamental problem in Intrusion detection is the fusion of dependent information sequences.In this paper ,we consider the fusion of two such sequences ,namely the sequence of system calls and the value of the instruction pointer.We introduce FAAD, a finite automation representation defined for the product alphabet of the two sequences where dependencies are implicitly taken into account by a matching procedure.},
	address = {Baltimore, Maryland},
	booktitle = {37th Conference on Information Sciences and Systems (CISS)},
	organization = {Johns Hopkins University}
}
@conference {
	title = {TORA, Verification, Proofs and Model Checking},
	author = {Yang, Shahan., Baras, John S.},
	year = {2003},
	month = {03/2003},
	address = {Sophia-Antipolis, France},
	booktitle = {WiOpt \&rsquo;03: Modeling and Optimization in Mobile, AdHoc and Wireless Networks}
}
