Analysis of LEACH Protocol(s) using Formal

Verification
A. Ihsan* and K. Saghar**
* National University of Science and Technology, Islamabad, Pakistan
** CESAT, Islamabad, Pakistan

Abstract— WSN nodes operate in an unattended A number of challenges are related with WSNs due
environment and thus have irreplaceable batteries. to the limited capabilities of low-cost sensor hardware
Thus an important concern is the network lifetime; and the necessity for sensor nodes to operate with only
we need to utilize their energy for a longer time a tiny irreplaceable battery for long periods of time.
otherwise nodes run out of power. For this purpose The focus is not to try to reduce the total consumed
various protocols have been established and the energy on the paths but to increase the lifetime of the
subject of our matter is the LEACH protocol. The network as long as possible. If sensor nodes utilize
LEACH protocol is self-organizing and is their energy in a more balanced nature, they provide
characterized as an adaptive clustering protocol increased connectivity and the life of the
which uses randomization to distribute energy load communication increases.
evenly. By using cluster heads and data aggregation Thus various protocols have been established to
excessive energy consumption is avoided. In this overcome this limitation and increase the network life
paper we analyzed LEACH and its extensions like time as long as possible to avoid replacing these small
LEACH-C and LEACH-F using Formal modeling batteries as sensor nodes often operate in inaccessible
techniques. Formal modeling is often used by environments.
researchers these days to verify a variety of routing Optimized distribution of energy load among the
protocols. By using formal verification one can network nodes is not guaranteed by classical
precisely confirm the authenticity of results and worst approaches like Direct Transmission (DT) and
case scenarios, a solution not possible using computer Minimum Transmission Energy (MTE) [1]. Using DT,
simulations and hardware implementation. In this sensors forward data directly to the BS, so sensor
paper, we have applied formal verification to compare nodes that are at a larger distance from the BS would
how efficient LEACH is as compared to its extensions die first [2]. Whereas by using MTE, data is routed
in various WSN topologies. The paper is not about over minimum cost routes, where cost is the
design improvement of LEACH but to formally verify transmission energy used. Nodes that are near the BS
its correctness, efficiency and performance as already act as relays. These nodes tend to die faster than the
stated. This work is novel as LEACH and its other nodes. The sensing of the field will be biased
extensions according to our knowledge has not been under both approaches as a part of the field will not be
analyzed using formal verification techniques. monitored for a significant life of the sensor network
[3]. A solution proposed in [1], called LEACH,
Index Terms—Wireless Sensor Networks (WSN), guarantees that energy is distributed evenly by making
Routing Protocol, Formal Modeling, Protocol dynamically created clusters, using a certain optimum
Verification, Hierarchal Networks probability.
In this paper this protocol is discussed and analyzed
I. INTRODUCTION and further compared with its extensions using a new
Wireless Sensor Networks (WSNs) research study formal modeling technique.
investigates the properties of networks of small battery- The rest of the paper is organized in the following
powered sensors that use wireless communication. way: section II briefly discusses related work; LEACH
These sensors are small, light weight and portable and protocol and its extensions are described in section III;
their significance appears from their efficiency in our formal framework is introduced in section IV and
detailed monitoring of remote and inaccessible the results and simulations are presented in section V.
locations where it’s not beneficial to install Conclusions and further work are presented in section
conventional wired framework. VI.
Each wireless sensor collects data from its
monitored domain area. Then it routes the collected II. RELATED WORK
data back to the base station. Data communication is Researchers have realized that computer simulation
usually multi-hop toward the base station using a is often inadequate for finding errors and corner cases
certain protocol. The number of nodes in a WSN may in routing protocols. It can be extremely difficult to
vary from a few to a few thousand. Unlike wired imagine the required system interactions and thus
networks, which have dedicated routers for testing becomes infeasible. Thus formal analysis
connectivity and forwarding data, each node in a WSN allows the designer to ask questions such as: Will this
can act as a router. ever happen? Whereas regular testing only allows for:

Proceedings of International Bhurban Conference on Applied Sciences & Technology

Islamabad, Pakistan, January 13 – 17, 2015
What happened? Therefore corner case analysis
through formal modelling indeed has an important
place in analysis and verification of sensor network
systems. Formal modelling is a fault avoidance
technique that helps in minimization of errors. They
accompany fault removal techniques like testing.
Formal modeling is not new and has also been used in
the analysis of different WSN protocols for example,
[18] analyzes TinySec and LEAP protocols; the formal Figure 1
analysis in [17] is performed on SNEP (SPINS) [15];
the work on [14] worked on uTESLA and LEAP
protocols. The work in [16] analyzes TinyOs, Direct
Diffusion, Rumour Routing, and Authentic TinyOS
with uTESLA. Finally ARAN protocol is analyzed in
[19]; Arrive protocol in [20]; INSENS protocol in [21]
and RAEED protocol in [22]. This paper further extend
this work and analyzes LEACH protocol and its
extensions using formal verification techniques.

III. DESCRIPTION OF THE PROTOCOL Figure 2

Algorithm for the decision:
A. LEACH: Formally speaking, the actual algorithm is that
each node generates a random number between 0 and
LEACH is the earliest proposed single-hop 1, and compares this number with the threshold value T
clustering routing protocol in WSN; it can save (n). If the number is less than T (n), the node is
network energy greatly compared with the non-cluster selected as a cluster-head, the threshold T (n) is set as
routing algorithm. This protocol falls under follows [5]:
𝑝
hierarchical networks. 1 𝑖𝑓 𝑛 Є 𝐺
1−𝑝∗ (𝑟 𝑚𝑜𝑑 )
It is self-organizing and is characterized as an T(n) = { 𝑝 (1)
adaptive clustering protocol which uses randomization 0 𝑖𝑓 𝑛 ∉ 𝐺
to distribute energy load evenly. This randomization is
induced by using a probability based algorithm which Where n refers to the node identification in the current
is discussed later. sensor network; p is the percentage of cluster-heads; r
Dense network of sensor nodes are grouped into is the current round number; G is the set of nodes that
clusters and each cluster consists of members called have not been elected as cluster-head in the last 1/p
Cluster Members or Normal Nodes and a coordinator round.
node called the Cluster-Head, CH. Cluster-heads Each node that elected itself a cluster-head for
consume more energy than non-cluster heads. current round broadcasts an advertisement message to
Whenever some emergency affairs happen in the rest of nodes using a CSMA MAC protocol as shown
monitoring area of a node it triggers the node which in Fig 2.
then sends its data to the Cluster-head. Cluster-heads Normal nodes must keep receivers turned on to
aggregate the data and forward the data to the Base hear advertisements from the cluster heads [4]
Station. The base station is fixed and away from the  After this phase, each node decides which cluster
sensors as shown in Fig. 1. to belong to for this round by choosing a cluster-
To go into detail, the communication process is head that a minimum distance from the node and
divided into rounds and each round can be divided into requires minimum transmission power as shown in
two phases, setup phase and the steady phase. Fig 3.
i. Setup phase:  Random cluster-head chosen in the case of ties.
(1) Advertisement phase:  If a node is out of the range of all Cluster-heads
then it sends its data on its own if it has the
In LEACH protocol each node decides required energy.
independently on its own whether it wants to be a CH
or not. Thus it uses a distributed approach. The
decision by every node to be a cluster-head depends
upon [4]:
 Percentage of cluster heads out of the total nodes
 How many times it has been a cluster head in the
previous rounds.

Proceedings of International Bhurban Conference on Applied Sciences & Technology

Islamabad, Pakistan, January 13 – 17, 2015
 Figure 3

(2) Cluster Set-up Phase:

After node picks its cluster it informs its cluster-

head as shown in Fig 4. Cluster-head now knows its
members & their identifiers.

Figure 6
Each node sends information about its current
location (using a GPS receiver) and energy level to the
BS, during the set-up phase of LEACH-C. In addition
to determining good clusters, the BS needs to ensure
that the energy load is evenly distributed among all the
nodes. [7]
Figure 4 Algorithm:
To do this, the BS computes the average node
energy, and whichever nodes have energy below this
ii. Steady Phase
average cannot be cluster heads for the current round.
Using the remaining nodes as possible cluster heads,
(1) Schedule Creation:
the BS finds clusters using the following algorithm:[8]
 CH then generates a TDMA schedule telling
each node when it can communicate its data MSD = Minimum Separation Distance
 Node i transmits once per frame dc = Number of desired cluster heads,
 Cluster head aggregates the data received from alive = Set of nodes alive,
nodes in the cluster. energy(n) = Remaining energy for node n
avg = ∑ energy(n) / number of alive nodes
CH= { }
eligible = {n| energy(n) >= avg }
assert(|eligible| >= dc)
While |CH| < dc
If ∃ n : n Є eligible Λ (∀ m Є CH, dist(m,n))>=MSD
Figure 5 add (n,CH)
remove (n,eligible)
(2) Data Transmission: Else
Each cluster head now forwards its data to the BS. n Є eligible
Also those nodes which are not in the range of any CH add (n,CH)
forward their data themselves to the BS if they have the remove (n,eligible)
required energy. Once the cluster heads and associated clusters
are found, the BS broadcasts a message that contains
Deficiencies in LEACH: the cluster head ID for each node. If a node’s cluster
The election of cluster head node in LEACH has head ID matches its own ID, the node is a cluster head;
some deficiencies such as, CH selection is random, otherwise, the node determines its TDMA slot for data
which does not take into account energy or some very transmission and goes to sleep until it is time to
big clusters and very small clusters may exist in transmit data. The steady-state phase of LEACH-C is
the network at the same time[9] thus various other identical to that of LEACH. [12]
extensions have been developed of LEACH which are
explained below. C. LEACH-F

B. Improvised LEACH-C: A further extension to these protocols is LEACH-F

(LEACH with Fixed clusters). As the name suggests
The main concept behind this protocol is that using LEACH-F is based on a single cluster selection and
a centralized control algorithm to form clusters may then the clusters are fixed and only the cluster head
result in better cluster formation by dispersing the position rotates within the cluster. Its significance is
cluster head nodes based on their location throughout that, once the clusters are determined, there is no set-up
the wireless network. This is the basis for LEACH- overhead at the beginning of each round. LEACH-F
centralized (LEACH-C). uses the same centralized algorithm as LEACH-C.
IV. FORMAL FRAMEWORK
A. LEACH

Proceedings of International Bhurban Conference on Applied Sciences & Technology

Islamabad, Pakistan, January 13 – 17, 2015
 The framework comprises of a model for the The first step is to express this informal definition
wireless medium and models representing wireless of the protocol as a series of formal equations. These
nodes acting in one of the following roles: BS (Base are then later transformed into a formal model.
Station) or node. The node could either be a CH The first would be the message sent by the normal
(Cluster Head) or a normal node which is different in nodes to their CH. The notation for this will be:
every round of the model. Each wireless node model is
instantiated from an Uppaal template that represents N  *{NID=gMember}: (gInformation, gMember)
the node behaviour as determined by the role in the
protocol. The notation is generally represented as A 
Each node model initially identifies itself as a B: M where node A transmits the message M to the
normal node or a CH. If it’s a normal node then it node B. A broadcast transmission is indicated by the
sends its data to the nearest CH. And if it’s a CH then it use of * in place of B indicating that message M is
waits for the data from its members. When every CH transmitted to all nodes within radio range of A. Here
has received its data from all its respective members NID = gMember indicates that if the receiving node
then they all forward it to the BS. has its NID equal to the global variable gMember then
The BS model receives data from all the fixed it should receive that information as it is the CH of that
number of cluster heads and increments the round node.
when it has received every CH’s data. ii. Formal Model

1. Our Approach The formal model of the node in the Figure 8

comprises of (i) a start location (ii) a decision point
The essence of our approach is to model the which separates the CH nodes from the normal nodes
protocol on a set of N nodes and to calculate the life (iii) mechanisms to sequentially send data from the
span of all our nodes. In order to keep simplicity first nodes to their respective CH (iv) a count to determine
we model a single round of the protocol and then carry if all the nodes have sent their data to their CH so that
on towards multiple rounds until all nodes are dead. the CH can then forward the data to the BS.
The formal model of the BS in the Figure 9
comprises of (i) a start location (ii) a loop to receive
2. Distance Matrix data from the two CH.

With the assumption that the distance between The node model starts at the initial state which
two consecutive nodes in our network is the same, a is the START state and calls several functions at the
distance matrix is an NxN matrix (where N is the total start of the round. The first being a global CH_Select()
number of nodes in the network) that represents the function. In the single round model, to keep it simple
distance between any two nodes. The matrix is of the CH are calculated simply by the following
course a symmetrical matrix as shown in the Table 1 formulas:
having used the example of 4 nodes numbered 0 – 3. CH1 = (gRound + 1) % gTotalNodes;
This matrix is representing the network in Fig 7. CH2 = (gRound + 6) % gTotalNodes;
Where gRound is the number of rounds completed
which would be 0 in this case, and gTotalNodes is the
number of nodes in the model, which is 4 for this
modelling example.
The next function is Cluster_Head(NID) this
function is called by every node to determine if its NID
is equal to CH1 or CH2; if it is then it sets its CH
Boolean to true for this round.
Table 1 Figure 7
iii. Modelling a Channel
This is known as the grid topology and it is
assumed that each node is at a fixed distance from its
Broadcast message passing in Uppaal
consecutive node. As that is an ideal situation and in
conveniently models WSN message passing. Whenever
real time scenarios that is not the case so we have also
data is sent “!” is used and to receive data “?” is used
used a topology matrix.
with the channel’s name. The channels are modelled
using global flags gChannelBusy1 and gChannelBusy2
3. Modelling a single round for Leach
which are used to indicate if the channel is busy or
free. These flags are used to check if a node is allowed
This section models a single round of the
to broadcast a message or not. gChannelBusy1 is used
Leach model thus there is no count of energy initially
by non-CH nodes which are sending their data to their
that would be accounted for in the full model.
respective CH which is closer to them. Non-CH nodes
i. Semi Formal Notations
are those whose lCH variable is false and thus go
towards right at the DECISION_POINT in the model.

Proceedings of International Bhurban Conference on Applied Sciences & Technology

Islamabad, Pakistan, January 13 – 17, 2015
Whereas gChannelBusy2 is used by the CH when it The function of the local variable lMemberCH
forwards its data to the BS. and global variable gMember is already explained in
As discussed a distance matrix is used to detail but in short they are used to tell their respective
indicate the mutual distance between any two given CH to receive their data. The nodes thus one by one
nodes. This matrix is thus used by the non-CH nodes to send data through the Data channel. On the other side
find out who is their respective CH. For this purpose the CH turns the gReceiver flag false so that the next
there is a function called Compare_Distance(NID) node does not send its data while this CH is in the
containing a local variable lMemberCH. This function RECEIVE state. When it returns to the
is called by every node at the start and if the node is not DECISION_POINT and is ready to receive data it
a CH then it calculates its distance from the two CH, turns this flag on. Also there is a global variable
and finds out which one is nearer and assigns that value gCount that increments whenever data is received and
to its lMemberCH. Thus whenever any normal node increments till gCount becomes equal to
sends data to its CH it sets the gChannelBusy1 flag and gNormalNodes which is given by:
then updates the global variable gMember equal to
lMemberCH to notify that CH that some node is gNormalNodes = gTotalNodes – gNumberOfCH
sending data to it. That CH checks if its NID is equal to
gMember and if it is then receives that data from it and which indicates that all the normal nodes have sent
turns gReceiver flag false so that the next node does their data to their respective CH.
not send its data while this CH is in the RECEIVE A gChannelBusy2 flag is used by all CH to
state. When it returns to the DECISION_POINT and is send the collective data one by one to the BS by using a
ready to receive data it turns this flag on. channel called gFwdData.
So each node calls Compare_Distance(NID) N  BS: (gInformation,FwdData)
and the non-CH nodes then determine their CH by
using distance_matrix[gTotalNodes][gTotalNodes] (a
2D array).
Next is a function presence(NID) which has a
global variable CHPresent which should be equal to
gNumberOfCH for any non-CH node to send data. This
variable increments whenever a CH reaches the
DECISION_POINT indicating that it is now ready to
receive data from its respective nodes one by one. Figure 9
The BS model consists of only two states
START and RECIEVE. The model is initially in the
START state and goes to receive when a CH sends its
data. Then it immediately returns to the START state
while calling Round_Increment() function where
gRound variable is incremented to indicate number of
rounds and a global gLoop is incremented, which when
becomes equal to gNumberOfCH makes gFwd equal to
true and thus the model goes in a self loop indicating
the end of the model to avoid a deadlock.
Figure 8 4. Modelling multiple rounds for Leach
When a node reaches the DECISION_POINT if its
lCH is true then it goes to the left otherwise right. First It can be seen that there are a lot of things
we look at the right side of the model for the non-CH added to execute multiple rounds. This is because
nodes. There is a global variable gCheck that serves nodes start to become dead and we have to handle
like a time slot and starts with 0 skips the CH nodes those situations.
and ends at gTotalNodes. By default gCheck is In multiple rounds LEACH the actual
incremented before SENSE but there is an Increment() algorithm for the LEACH protocol is applied. This
function that increments gCheck again in order to skip algorithm is applied in the CH_Selection(NID,r)
the CH and not give a time slot to it. method. Once the cluster-head is determined, the
There is a global gReceiver variable that is cluster-head sends a broadcast message to the network,
used to indicate if the CH is ready to receive the data announced itself as the cluster-head; each normal node
from a normal node or not. It will be further explained decides which cluster to join in according to the signal
when explaining the left side of DECISION_POINT. strength of the received message, sends a request
As explained in section 3.2.6.4 gChannelBusy1 is used message to the corresponding cluster-head.
to check if the channel is busy or not. gCHPresent
indicates both CH are present beyond
DECISION_POINT.

Proceedings of International Bhurban Conference on Applied Sciences & Technology

Islamabad, Pakistan, January 13 – 17, 2015
 As stated before the energy has been
decremented in the multiple rounds model. The energy
is decremented for each node whenever it sends its
data. The three types of energy depletions are:
 When a node sends its data to a CH energy is
decremented according to the equation (2) and
written in the Energy_transmission(l,NID)
function.
 When a CH forwards its data it decrements a fixed
energy which is much larger than for the normal
nodes.
 Some energy is decremented in the model for the
data receiving part.
Due to these energy depletions there would come a
Figure 10 time when nodes start to become dead and so certain
A structure is now also used to represent each transitions have to be made to cater for the dead nodes.
node. This array of structures is used because for the A dead node can be of two types:
tdma schedule slots are allotted to each node to send  A CH, if that is the case then all data is lost and the
data to its respective CH. These slots are represented round resets back to the START and all variables
by this array of structures and are incremented in each are reinitialized.
cycle to send their data.  A normal node, in that case the model should
The Initialize(NID) function contains the continue working without any error.
CH_Sorter(), Compare_Distance(NID), Presence(NID) When any node becomes dead it increments a
functions. First the CH_Sorter() function sorts the array variable gCountDead which would be used in the
of structures in such a way that all the CH are present verification part of our analysis. It also decrements the
at the start followed by the normal nodes as explained gIndex value.
in the Figure 11 and Figure 12 B. Improvised LEACH-C model

Node 0 1 2 3 4 5 6 7 The LEACH-C model has been derived from the

ID LEACH model. The only difference is in the CH
CH T F T T F F F T Selection as LEACH uses a distributed approach and
LEACH-C uses a centralized approach where all CH
Figure 11 are selected by the BS.

So each node sends its energy and location

Node 0 2 3 7 1 4 5 6
information through the channel info!. The BS receives
ID
each information in a loop and calculates the CH in the
CH T T T T F F F F CH_select function of the BS. The CH are selected
based on the algorithm in section III b. Then after that
Figure 12 calculation this information is sent to each node by the
Then in the Compare_Distance function all channel cluster! and so each node now knows whether
nodes with CH value false check the gTopologyMatrix it is a CH or a normal node. The rest of the mechanism
to find out their CH and make their lMemberCH equal remains the same.
to that ID as already explained before. If a normal node
is not connected to any CH directly then it has to send 1. Semi-formal Notation:
data on its own and its lMemberCH becomes equal to When nodes send data to their BS the notation is:
its own NID and it turns a Boolean lSkip true. N  BS: (info)
gCheck now becomes equal to
gTDMA[gNumOfCH] as that is the first normal node. When a BS sends its data to all nodes the notation
In Figure 12 node 1 is the first normal node to send would be
data. Thus now nodes send data in this order as in BS  N: (cluster)
Figure 13. This is known as the TDMA schedule
followed by the nodes to send their data to their C. LEACH-F model
respective CH.
The LEACH-F model is derived from the
1 4 5 6 LEACH-C model. The first difference is that in
LEACH-F only in round 0 the Clusters are made by the
False False False False BS. Thus on the first transition of the START state the
guard now also contains the condition gRound == 0.

Figure 13

Proceedings of International Bhurban Conference on Applied Sciences & Technology

Islamabad, Pakistan, January 13 – 17, 2015
 Another difference is that now CH are selected
from these already made clusters one by one based on
energy and number of times they were made CH
before. For this purpose cluster_id and cluster_same
are added to the model.

1. Semi-formal Notation:
It remains the same but only applies in the first
round.

V. Results and simulations

Different graphs are drawn on the basis of: Figure 16

 The maximum number of rounds any topology
within the range can have Following graph shows that in which round
 The minimum number of rounds the whole range first node becomes dead in worst case scenario and in
of topologies should satisfy which round first node becomes dead in the best case
 The round at which in any topology a first node scenario.
becomes dead.

Figure 17

Figure 14 Above graph shows LEACH-F depicts more

From above graph, LEACH-C and LEACH-F even and constant behavior i.e. number of round in
show consistent behavior. Graph depicting same thing which first node dead in both scenario is same but
but with different energy given to node i.e. 1000 LEACH-C also shows good outcome as first node dies
very late in both scenarios.

Figure 15

Similarly for energy 1450, the graph is shown Figure 18

below This graph shows that in LEACH there is a
percentage of packet drops whereas in LEACH-C and
LEACH-F there is no drop packets. So in terms of
throughput LEACH-C and LEACH-F are more stable
protocols.

Proceedings of International Bhurban Conference on Applied Sciences & Technology

Islamabad, Pakistan, January 13 – 17, 2015
 [5] Clusterhead selection in clustering algorithms for
wireless sensor networks: a
survey,” inProceedings of the International Conference
on Computing, Communication and Networking
[6] Formal modelling and analysis of routing protocol
security in wireless sensor networks
[7]
http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=
1045297&url=http%3A%2F%2Fieeexplore.ieee.org%2
Fxpls%2Fabs_all.jsp%3Farnumber%3D1045297
[8] Efficient Cluster Formation for Sensor Networks
Figure 19 Ewa Hansen, Jonas Neander, Mikael Nolin and Mats
Bj ¨ orkman
Above graph shows that LEACH depletes the [9]
most energy whereas LEACH-C and LEACH-F utilize http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumb
the energy more efficiently than LEACH. er=5760277
[10]
VI. Conclusion http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumb
er=5546247
In this paper we have critically analyzed [11]
different LEACH extensions in various WSN http://www.hindawi.com/journals/ijdsn/2012/649609/
topologies. The LEACH protocol is self-organizing and [12]
is characterized as an adaptive clustering protocol http://210.32.200.159/download/20130923134204903.
which uses randomization to distribute energy load pdf?&session-id=ab41608ddbbefeeac23e3aa0c55dad9c
evenly. By using cluster heads and data aggregation [13] A. Wood and J. Stankovic. Denial of service in
excessive energy consumption is avoided. In this paper sensor networks. In IEEE Computer, volume 35, pages
we analyzed LEACH and its extensions like LEACH-C 54–62, Sep 2002.
and LEACH-F using Formal modeling techniques. By [14] Y. Hanna, H. Rajan, andW. Zhang. Slede: a
domain-specific verification framework for sensor
using formal verification one can precisely confirm the
network security protocol implementations. In
authenticity of results and worst case scenarios, a Proceedings of the first ACM conference on Wireless
solution not possible using computer simulations and network security (WISEC 2008), Alexandria, VA, USA,
hardware implementation. This work is novel as pages 109–118, 2008.
LEACH and its extensions according to our knowledge [15] A. Perrig, R. Szewczyk, V. Wen, D. Culler, and J.
have not been analyzed using formal verification Tygar. SPINS: Security Protocols for Sensor Networks.
techniques. We analyzed the protocols against worst In ACM Mobile Computing and Networking, volume 8,
and best scenarios in terms of energy, life (first node pages 521–534, Sep 2002.
dead etc) and throughput. Our verification results [16] K. Saghar,W. Henderson, and D. Kendel. Formal
modeling and analysis of routing protocol security in
confirmed that the results go mostly in the favor of
wireless sensor networks. In PGNET 2009,Liverpool,
LEACH-F. Thus we can safely say that LEACH-F is UK, pages 179–184, 22-23 June 2009.
best among these extensions. We intend to test more [17] L. Tobarra, D. Cazorla, and F. Cuartero. Formal
LEACH extensions and WSN protocols in future using Analysis of Sensor Network Encryption Protocol
the same technique. (SNEP). In IEEE Internatonal Conference on Mobile
Adhoc and Sensor Systems (MASS 2007), Piscataway,
References NJ, USA, pages 767–772, Pisa (Italy), October 2007.
[1] [18] L. Tobarra, D. Cazorla, F. Cuartero, G. Diaz, and
http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber= E. Cambronero. Model Checking Wireless Sensor
Network Security Protocols: TinySec + LEAP. In Proc.
1045297&url=http%3A%2F%2Fieeexplore.ieee.org%2
of the First IFIP International Conference on Wireless
Fxpls%2Fabs_all.jsp%3Farnumber%3D1045297 Sensor and Actor Networks (WSAN’07), pages 95–106,
Albacete (Spain), September, 2007. IFIP Main Series,
[2] Springer.
http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber= [19] K. Saghar, W. Henderson, D. Kendall, and A.
926982&url=http%3A%2F%2Fieeexplore.ieee.org%2 Bouridane. Applying formal modelling to detect
Fxpls%2Fabs_all.jsp%3Farnumber%3D926982 DoS attacks in wireless medium. In IEEE, IET
International Symposium on COMMUNICATION
[3] SEP: A Stable Election Protocol for clustered SYSTEMS, NETWORKS AND DIGITAL SIGNAL
heterogeneous wireless sensor networks PROCESSING NASA/ESA(CSNDSP 2010),
[4] 2010.
http://www.cs.gsu.edu/yli/teaching/Fall10/sensor/Slide [20] K. Saghar, W. Henderson, D. Kendall, and A.
s/rp.pdf Bouridane. Formal modelling of a robust wireless
sensor network routing protocol. In NASA/ESA

Proceedings of International Bhurban Conference on Applied Sciences & Technology

Islamabad, Pakistan, January 13 – 17, 2015
Conference on Adaptive Hardware and Systems
(AHS-2010), 2010.
[21] K. Saghar, D. Kendall, and A. Bouridane.
Vulnerability of INSENS to denial of service
attacks. In 36th International Conference on
Acoustics, Speech and Signal Processing
(ICASSP 2011), Praha, Czech Republic.
[22] K. Saghar, D. Kendall, and A. Bouridane.
Automatic detection of black hole attack in
wireless network routing protocols. In IEEE,
International Bhurban Conference on Applied
Sciences & Technology Islamabad, (IBCAST
2014) Pakistan, 2014.

Proceedings of International Bhurban Conference on Applied Sciences & Technology

Islamabad, Pakistan, January 13 – 17, 2015