Logic-Based Security Architecture for Systems Providing Multihop Communication

Abstract

Security is a basic element of distributed systems such as ad hoc and sensor communication networks. Several standards define security requirements and enforcers, such as ITU-T Recommendations X.800 and X.805. It is essential to specify and analyze protocols to know which security requirements they achieve. This paper presents a logic-based security architecture (LBSA). LBSA is a systematic way to test if a protocol is secure by checking what security requirements are achieved. Different rules, actions, and sets which fit into the proposed LBSA are included, new ones are also added to complete the architecture. The key advantage of LBSA is that it enables a security protocol to prove its correctness mathematically. Mathematical proofs provided by LBSA cover more cases that usually cannot be covered exhaustively by simulation tools. This paper also specifies and analyzes several security enforcers and protocols and mathematically proves which security requirements they achieve. Mapping between security requirements and inference rules/actions is also provided to facilitate the use of LBSA. Some enforcers are analyzed using LBSA to demonstrate how they achieve security requirements. Finally, we take Ariadne protocol as a case study and show how to use the proposed LBSA architecture to prove that this protocol is secure.

1. Introduction

When two entities communicate to obtain a certain service(s), they must ensure secure end-to-end communication. Systems do not provide efficient services without applying proper security mechanism due to the existence of different types of attackers. Security can be defined through a set of requirements that must be achieved by the communicating parties to communicate securely and protect services from attackers.

Because of the importance of security for end-to-end communication, many secure protocols have been proposed as will be discussed later in the paper. Some of these protocols had taken prevention measures to stop attackers while others had taken the detection approaches. A way to analyze these protocols is required to check if these protocols are secure as their designers claim and to know which security requirements these protocols achieve. In this paper, we propose a logic-based security architecture (LBSA) which is an easy, fast, and reliable way to specify and analyze secure protocols.

Some security requirements, as defined by several standards such as ITU-T Recommendations X.800 and X.805 [1, 2], must be achieved to declare that a protocol is secure. Using LBSA, a protocol can be tested to check which security requirements it achieves. Several efforts have been done to utilize logic in such test [3–8], but logic was used to specify and analyze specific protocols by defining global and local sets, actions, and inference rules. In this paper security architecture is taken as a whole, different actions, sets, and rules which fit into the architecture have been included, that means specifying and analyzing different enforcers and determining the requirements they satisfy. Also, we had labeled the actions, sets and rules for easy access and we added our own to complete the architecture. Additionally, we mapped different security requirements into inference rules/actions. This mapping shows the inference rules/actions which are used during the protocol analysis to achieve security requirement(s).

Utilizing LBSA, protocols can be tested to check if they achieve the security requirements specified by their designers. This checking can be performed by analyzing the protocol and applying appropriate actions and rules. If the rules are applied successfully we conclude that their claim is true, otherwise it is false.

The rest of this paper is organized as follows: Section 2 illustrates the security architecture. Section 3 presents related work. Section 4 presents the proposed Logic-Based Security Architecture (LBSA) for systems providing multihop communication. Section 5 provides possible mapping between security requirements and inference rules/actions. In Section 6, the specification and analysis of message authentication code (MAC) and digital certificate based on LBSA are discussed. Section 7 illustrates how to specify and analyze protocols using LBSA by taking Ariadne routing protocol as a case study. Finally, Section 8 concludes the paper and presents avenues for future work.

2. Security Architecture

Security architecture as defined by ITU-T Recommendations X.800 [1] and X.805 [2] defines a set of security requirements that must be achieved. Figure 1 illustrates this architecture.

Figure 1

Security Architecture extracted from ITU-T Recommendations X.800 and X.805.

Security architecture as shown in Figure 1 includes a set of security requirements that are used to protect systems from different types of attackers. To achieve the objectives of these requirements, a set of security enforcers must be applied.

The requirements and their definitions are illustrated as the following.

• (i)

Authentication: Prove the identity of the communicating parties.

(ii)

Authorization: control the access to the system's resources. Give different entities different privileges according to their roles.

(iii)

Confidentiality: ensure the secrecy of data. Secret data must be read only by intended recipients.

(iv)

Integrity: protect the received data from any kind of modifications during transmission from the sender to the receiver.

(v)

Nonrepudiation: prevent the users from denying the sending of messages or initiating events that they had performed.

(vi)

Privacy: protect the identity and/or the location of the node and sometimes the routing protocol being used.

(vii)

Availability: ensure that no one prevents authorized users from getting access to the system available services.

These requirements must be achieved to guarantee secure communication and to prevent and detect different attackers which can be classified into the following.

• (i)

Internal or external attackers: internal attackers are compromised users who are authorized to enter the system but they are misbehaving. This type of attack needs a detection mechanism to be discovered as they have the authority to access the system's services. External attackers, on the other hand, are unauthorized entities attempting to access the system's services; these attackers must be prevented from accessing the system's resources.

(ii)

Passive or active attackers: passive attackers monitor the system without taking any action and usually it is a phase that precedes an active attacking. Active attacker takes actions and does modifications.

(iii)

Intentional or accidental: intentional attack is a planned attack while accidental attacking results from system malfunctions such as software bugs.

Several mechanisms and techniques have been defined to achieve different security requirements. Table 1 gives examples of different security enforces that are used to implement the objectives of different security requirements.

Table 1

Examples of security requirements enforcers.

Security requirement	Security enforcer
	(i) Digital certificate
Authentication	(ii) Digital signature
	(iii) Message authentication code (MAC)
Authorization	Firewall
Confidentiality	Encryption
	(i) Hash function
Integrity	(ii) MAC
	(iii) Digital signature
Nonrepudiation	Digital signature
	(i) Achieved partially by encryption
Privacy	(ii) Hide node location
	(iii) Hide node identity
	(iv) Hide routing protocol
Availability	(i) Intrusion detection scheme (IDS)
	(ii) Intrusion prevention scheme (IPS)

Secure protocols usually use the above enforces, among others, to achieve the security requirements. There are different ways to analyze security protocols in terms of achieved security requirements such as simulation and mathematical models; this paper uses logic to do such analysis.

3. Related Work

The importance of security in providing successful services in any distributed system raises the necessity of having formal way to analyze security protocols. Previous effort in using logic for analyzing security is Rubin logic [3, 4].

Rubin logic is an approach that specifies and analyzes nonmonotonic cryptographic protocols. It is one of the first approaches to allow reasoning about nonmonotonic protocols [3]. In nonmonotonic protocols, beliefs are changed during protocol execution time. An example of nonmonotonicity is the belief that a key must be changed when a node becomes compromised. To achieve the protocol specification and analysis, Rubin logic defines global and local sets, actions and inference rules.

Rubin and Honeyman [3] focused on authentication protocols. They took KHAT protocol [9] as an example to discover its flaws. KHAT protocol was built to solve the problem of long running jobs in an authenticated environment where a trusted server issues tickets with limited lifetimes for services. The authors gave special attention to ensure the freshness of data using fresh nonce. The main problem they attempted to solve is that principal B cannot achieve the belief that the session key with principal A is fresh. Finally, the authors defined most of global and local sets that are used later in the literature.

Rubin [4] extended the work presented in [3] by adding one set. Rubin [4] aimed to make sure that keys are observed by their intended parties and data items are fresh, especially the public keys. Rubin [4] made link between certificates and requests which reveals weakness in Needham and Schroeder public key protocol [10].

Xu and Xie presented in a series of papers [5–8] the utilization of Rubin logic in analyzing the security for specific protocols.

In [5], Xu and Xie extended the work presented in [4] to analyze nonrepudiation in routing protocols proposed for wireless mobile ad hoc networks (MANET). This work took ARAN [11] routing protocol to test nonrepudiation.

Xu and Xie [6] use the work presented in [5] to analyze electronic commerce protocols and in [7] they have chosen Zhou-Gollmann [12] protocol which is a simple and effective nonrepudiation protocol to illustrate how an electronic commerce protocol is analyzed using the extended Rubin logic.

Two examples of Rubin logic's applications are given by Xu and Xie in [8]. First example is the Andrew secure RPC [13] protocol using symmetric keys. The second one is X.509 [14] authentication protocol using asymmetric keys.

As can be illustrated from the above-related work, all attempts to utilize Rubin logic have either focused on a specific requirement or a specific protocol. This paper proposes a logic-based security architecture (LBSA) that presents a formal way to analyze any security requirement in any system providing multihop communication. All sets, actions, and rules presented in previous efforts are considered and generalized; new ones are added to complete the architecture. After that, we illustrate how LBSA will be used to test security requirements and issues in different security enforcers and protocols.

4. Logic-Based Security Architecture (LBSA) for Systems Providing Multihop Communication

In this section we illustrate the proposed architecture which defines a logical way for specifying and analyzing different enforcers and different protocols that achieve any security requirement as defined in [2]. Some researchers used logic as mentioned earlier in Section 3. All sets, actions, and rules defined in [3–8] which fit in our architecture have been included and labeled by the proposed LBSA.

Global sets define the specification of the protocol as a whole. Local sets are private to each principal in the specification. Actions are specified as part of the protocol (i.e., how the protocol works) while inference rules are used to reason about the beliefs during the protocol executing. Consequently, the relation between sets, actions, and rules and the result of the action may update the sets. This achieves some rules and conditions which are followed by applying inference rules which in turn update another set(s). Figure 2 shows this relation.

Figure 2

Relation between sets, actions and inference rules.

Using different actions, the protocol can be specified exactly as it works. While executing these actions, local and global sets will have new values which lead to applying some rules. This is the process of analyzing protocols.

The purpose of LBSA is to generalize rules and actions and not to specify them. Accordingly, these rules and actions can be customized according to the context. Sections 6 and 7 illustrate how these sets, rules, and actions can be customized according to the context. Additionally, each set, rule, and action are described in the following tables using the description column.

Table 2 defines different global and local sets. Global sets are labeled as $\text{G}{\text{S}}_i$ and local sets are labeled as $\text{L}{\text{S}}_i$ , where i is the set number. These sets contain the protocol information. There are five global sets $\text{G}{\text{S}}_1$ – $\text{G}{\text{S}}_5$ and ten local sets $\text{L}{\text{S}}_1$ – $\text{L}{\text{S}}_{10}$ . These sets have initial values and these values are changed whenever actions and rules are executed. Global sets ( $\text{G}{\text{S}}_1$ – $\text{G}{\text{S}}_4$ ) were initilly defined in [3] for a specific protocol called KHAT [9]. These global sets have been generalized by LBSA and new global sets are also added. Local sets ( $\text{L}{\text{S}}_1$ – $\text{L}{\text{S}}_8$ ) were initially defined in [3–5] for specific protocols, but they are generalized and labeled by LBSA which also defines new local sets needed to complete the architecture.

Table 2

Global and local sets of LBSA.

Set label	Set name	Description
GS1	Principal set	All principals (i.e., nodes) participate in the protocol are in this set. P = $\{P_1,P_2,\dots ,P_n\}$ . There is one initiator of the protocol and it could be any $P_i$ .
GS2	Rule set	Inference rules needed to derive new statements from existed assertions that are in this set. R = $\{R_1,R_2,\dots ,R_n\}$ , where $R_i$ is of the form $\left(C_{\mathrm{1}},C_{\mathrm{2}},\dots ,C_n\right)/D$   $C_i$ is a condition and D is a statement.
GS3	Secret set	Each secret in the system exist in this set. During the analysis, the content of this set will be changed for the emergence of new secrets such as session keys. $S=\{S_1,S_2,\dots ,S_n\}$ .
GS4	Observers set	For each $S_i$ , observers ( $S_i$ ) contain all the principals who could possibly know the secret $S_i$ by listening to network traffic or generating it themselves. The members of the Observers set can be stated explicitly or maintained as formulas representing their membership.
GS5	FireWall set( $P_i$ )	This set presents the firewall list that contains the access control rules that are needed to be applied to the incoming packets of $P_i$ in order to allow or prevent them.
LS1	Possession set( $P_i$ )	This set contains all the data relevant to security that this principal knows or possesses. This includes secret encryption keys, public keys, data that must remain secret, and any other information that is not publicly available. POSS( $P_i$ ) = $\{{\text{poss}}_1,{\text{poss}}_2,\dots ,{\text{poss}}_n\}$ . Note: ${\text{poss}}_i$ contains two fields—the actual data and the origin of this data.
LS2	Belief set( $P_i$ )	This set contains all the beliefs held by a principal. This includes the belief that the keys it holds between itself and other principals are good, beliefs about jurisdiction, beliefs about freshness, and beliefs about the possessions of other principals. BEL $(P_i)=\{{\text{bel}}_1,{\text{bel}}_2,\dots ,{\text{bel}}_n\}$ .
LS3	Opaque( $P_i$ )	This set contains candidates to be added to the Seen set. It is used by the Update function (Table 3(b)). The set contains text parts (data) of the message and a list of the associated keys needed to read them.
LS4	Seen( $P_i$ )	This set contains text parts (data) that $P_i$ sees from messages sent across the network. The Seen sets collectively contain the same information as the observers set.
LS5	Haskeys( $P_i$ )	This set contains keys that $P_i$ sees either because they are in the initial possession set, or because they appear in a message sent across the network and are added to $P_i$ 's seen set.
LS6	Behavior list( $P_i$ )	This item is a list rather than a set because the elements are ordered. BL $=\{\mathrm{AL},{\text{bvr}}_1,{\text{bvr}}_2,\dots ,{\text{bvr}}_n\}$ . AL is an action list as will be defined below.
LS7	Bindings set( $P_i$ )	This set contains the legal bindings of keys held by a principal. These are bindings that are created by $P_i$ , and bindings that are received in certificates from trusted servers. Bindings $(P_i)=\{k_1\bowtie P_1,k_2\bowtie P_2,\dots ,k_n\bowtie P_n\}$ .
LS8	Proofs set( $P_i$ )	This set contains all the other principals' nonrepudiation that $P_i$ can prove.
LS9	PL( $P_i$ )	Principals list contains all the principals that must receive Messages (Msgs) from principals $P_i$ .
LS10	AbnBeh( $P_i$ )	Abnormal behavior set contains all the principals that $P_i$ detect their abnormal behaviors.

Tables 3(a)–3(c) define the LBSA actions with their descriptions, conditions, and results. Actions are labeled as ${\text{ACT}}_i$ , where i is the action number and these tables contain 30 actions. The actions describe the node operations such as sending messages, receiving messages, generating key pairs among other operations. Actions ( $\mathrm{AC}{\text{T}}_1$ – $\mathrm{AC}{\text{T}}_{21}$ ) that are considered in [3–6] had been generalized and fitted in the proposed LBSA. Moreover, new actions are defined and added by LBSA.

Table 3

(a) Actions (ACT₁–ACT₁₀) of LBSA, (b) actions (ACT₁₁–ACT₂₀) of LBSA, and (c) actions (ACT₂₁–ACT₃₀) of LBSA.

(a)
Action label	Action name	Description	Condition	Result
ACT1	Send( $P_j$ , X)	$P_i$ sends msg X to $P_j$ .	—	Principal $P_i$ sends msg X to $P_j$ .
ACT2	Receive( $P_j$ , X)	$P_i$ receives msg X from $P_j$ .	—	Principal $P_i$ receives msg X from $P_j$ .
ACT3	Encrypt( $X,k$ )	If $P_i$ possesses msg X and knows the key k then it can encrypt X using k and possess ${\left\{X\right\}}_k$ .	$X,k\in$ $\text{POSS(}{P}_i),P_i\in$ Observers (k).	POSS( $P_i$ ) = POSS( $P_i)\cup \{{\left\{X\right\}}_k\}$ .
ACT4	Decrypt( ${\{X\}}_k$ , k)	If $P_i$ possesses msg X which encrypted under k and knows the key k (symmetric encryption) or its inverse (Asymmetric encryption), then $P_i$ can decrypt X and possess it.	$P_i\in$ Observers $(k),{\left\{X\right\}}_k$ , $k\in \text{POSS(}{P}_i)$ .	POSS( $P_i$ ) = POSS( $P_i)\cup \{X\}$ .
ACT5	Generate-nonce(N)	Is used to check out the freshness. A principal generates a nonce to link a challenge and a response. When the response is received, LINK(N) is removed from BEL( $P_i$ ).	—	POSS( $P_i$ ) = POSS( $P_i)\cup \{N\}$ , BEL( $P_i$ ) = BEL $(P_i)\cup \text{LINK}(N)$ .
ACT6	Generate-secret(s)	Is used to generate a new secret s. Note that the Observers set will be updated.	—	S:= $S\cup \{s\}$ ,  Observers $(s)=\{P_i\}$ ,  POSS( $P_i$ ) = POSS( $P_i)\bowtie \{s\bowtie P_i\}$ ,  BEL $(P_i)=$ BEL( $P_i)\cup$ #(s),  where $\#\hspace{0.17em}\hspace{0.17em}indicates$ that the value is fresh.
ACT7	Concat( $x_1,x_2,\dots ,x_n$ )	Is used to construct a message X out of submessages $x_1,x_2,\dots ,x_n$ .	$x_1,x_2,\dots ,x_n\in$ POSS( $P_i$ ).	POSS( $P_i$ ) = POSS( $P_i)\cup \{x_1,x_2,\dots ,x_n\}$ .
ACT8	Split(X)	When a message contains a set of components, this action is used to break it into its components.	X contains $x_1,x_2,\dots ,x_n$ ,  $X\in$ POSS( $P_i$ ).	POSS( $P_i$ ) = POSS( $P_i)\cup \{x_1,x_2,\dots ,x_n\}$ .
ACT9	Forget(X)	When $P_i$ no longer in possession of X, this action will be used. If other principles trust $P_i$ then they can believe that $P_i$ is no longer possesses X.	$X\in$ POSS( $P_i$ ).	POSS( $P_i)$ = POSS( $P_i)-\{X\}$ , $\forall P_j\in P$   if TRUST $[j,i]=1$ .   then BEL $(P_j)=\text{BEL}(P_j)-X\in$ POSS $(P_i)\}$ .
ACT10	Check-freshness(X)	Is used to verify the freshness of timestamp X.	$X\in$ POSS( $P_i$ ), X is not expired.	BEL( $P_i$ ) = BEL $\left(P_i\right)\cup \{\#(X)\}$ .

(b)
Action label	Action name	Description	Condition	Result
${\text{ACT}}_{11}$	Forget-secret(s)	When $P_i$ no longer knows the secret s. If other principals trust $P_i$ then they can believe that $P_i$ no longer possesses s.	$P_i\in$ Observers (s), $s\in$ POSS( $P_i$ ).	Observers(s) = Observers $(s)-\{P_i\}$ ,   POSS( $P_i$ )= POSS( $P_i)-\{s\},\forall P_j\in P$   if TRUST $[j,i]$ = 1 then BEL $(P_j)$ = BEL $(P_j)-\{s\in \text{POSS(}{P}_i)\}$
ACT12	Apply(f, X)	Is used to apply function f to X.	$f,X\in \text{POSS}(P_i$ ).	POSS( $P_i$ ):= POSS( $P_i)\cup \{f(X)\}$ .
ACT13	Abort	The protocol aborts when different cracks and events that affect the protocol specification happen.	Protocol run is illegal.	Analysis reports failure.
ACT14	Generate-key-pair( $k^{+},k^{-}$ )	Is used to generate two keys $k^{+}$ (public) and its inverse $k^{-}$ (private).	—	POSS( $P_i)=$ POSS( $P_i)\cup \{k^{+}\bowtie P_i,k^{-}\bowtie P_i\}$ .
ACT15	Apply-Asymkey(X, k)	There are two cases for applying asymmetric key operation on X. The first one when X is in the form of ${\{Y\}}_{k’}$ and k and $k’$ are inverses to each other. The second case when X is encrypted using k.	$X,k\in \text{POSS}(P_i)$ ,  $P_i\in$ Observers $(k)$ ,  k is an asymmetric key.	if   $X={\{Y\}}_{k’}$   and       k is the inverse of $k’$ ,   then  POSS( $P_i$ ) = POSS( $P_i)\cup Y$   else  POSS( $P_i$ ) = POSS( $P_i)\cup \{{\{X\}}_k\}$ .
ACT16	Bind( $k,P_j$ )	Before sending a key, principal $P_i$ can bind this key to other principle $P_j$ using this action. After this binding, both $P_i$ 's possession and Binding sets will contain $k\bowtie P_j$ .	$k\in$ POSS( $P_i)$ ,  $P_i\in \text{Observers}(k)$ ,  k is a key intended for $P_j$ .	POSS( $P_i)=$ POSS( $P_i)\cup \{(k\bowtie P_j)\}$ ,   Bindings  $(P_i)=$ Bindings $(P_i)\cup \{(k\bowtie P_j)\}$ .
ACT17	Update(X)	After sending a message this action is used to maintain the observers set.	—	Maintains the observers of X.
ACT18	Broadcast(X)	Message X is broadcasted by $P_i$ to each of its neighbors.	—	$P_i$ broadcasts X to each of its neighbors.
ACT19	Check-certificate( ${\text{cert}}_R$ )	Is used to verify the freshness of the certificate ${\text{cert}}_R$ .	${\text{cert}}_R\in$ POSS( $P_i)$ ,  ${\text{cert}}_R$ is not expired	BEL $(P_i)$ = BEL $(P_i)\cup \{\#(K_R)\}$ ,   where   $K_R$   is the public key specified in ${\text{cert}}_R$ .
ACT20	Check-request $(\{{\text{IP}}_R,N_R\})$	Is used to record new routing record. Each node receives route discovery packet it records the predecessor of that packet and the successor toward the destination.	${\text{IP}}_R$ ∈ POSS( $P_i)$ ,  $N_R\in$ POSS( $P_i$ ),  and $\text{{I}{\text{P}}_R\text{,\hspace{0.17em}\hspace{0.17em}}{N}_R\}$ is not already seen.	{new routing record $\}\in$ POSS( $P_i)$   Where: $\text{I}{\text{P}}_R$   is  IP  address of principle R  and $N_R$   is nonce of principle R.

(c)
Action label	Action name	Description	Condition	Result
ACT21	Comp(A, B)	This action is used to compare two values if they are equal or not.	A, B ∈ POSS( $P_i)$ .	If A and B are equal: ${\{X\}}^{*}\in$ Proof ( $P_i$ ),   means message X is checked and not modified   If they are not equal: POSS( $P_i)=$ POSS( $P_i)-\{X\}$ means message X is checked and it is modified
ACT22	Renew-key-pair( $k^{+},k^{-}$ )	This action is used to renew the public and private keys.	—	POSS = (POSS( $P_i)-\{k^{+}\bowtie P_i,k^{-}\bowtie P_i\})\cup \{\#k^{+}\bowtie P_i,\#k^{-}\bowtie P_i\}$ .
ACT23	Multicast( $\forall P_i\in$ PL, X)	It means that Principle $P_i$ sends msg X to all principles in the PL.	—	Principle $P_i$ sends message X to all principles in the PL.
ACT24	Modify( ${\text{Cert}}_R$ )	This action modifies certificate content.	—	Modify the certificate content.
ACT25	Monitor ( $P_i$ , abnormal behavior)	It means that principle $P_i$ monitors the abnormal behavior of other principals.	—	Principal $P_i$ detects abnormal behaviors of other principal $P_i,P_j\in$ AbnBeh( $P_i$ ).
ACT26	Generate-Alert( $P_i,P_j$ )	$P_i$ generates an alert at time t because it detects abnormal behavior of $P_j$ .	$P_j\in$ A bnBeh  $(P_i)$ .	Alert( $t,P_i,P_j$ )
ACT27	Alert-Filtering (Alert( $t,P_i,P_j$ ))	This action is used to do the process of categorizing attack alerts produced from principals in order to distinguish false positive from actual attack.	Alert( $t,P_i,P_j)\in$ POSS( $P_n)$ ,  where $P_n$   is any Principle $\in P$ ,  but not $P_i$ or $P_j$ .	If true positive $P_n$ takes an action.
ACT28	Access (Resource)	This action is used to allow or deny the access of resources.	AccessInfo $(P_i)\in$ FireWall, Condition = Allow	Allow resource access.
ACT29	$X\leftarrow Y$	This action is used to rename value Y to X.	$Y\in$ POSS( $P_i$ )	X ∈ POSS( $P_i)$ , Use X instead of Y.
ACT30	Process (Pra, Fun)	This action is used in key agreement process. Process parameters received from $P_j$ .	Fun ∈ POSS( $P_i$ ), parameters received from $P_j$ .	Key ∈ POSS( $P_i$ )

Different inference rules are defined in Tables 4(a)–4(d). $\text{R}{\text{L}}_i$ is the rule label where i is the rule number. As the rule conditions are executed correctly, the sets' values will be changed or the protocol will be aborted. Rules defined for specific protocols in [3–6] had been extracted, generalized, and mapped to LBSA. New rules were also generated by LBSA to complete the security architecture.

Table 4

(a) Rules (RL₁–RL₆) of LBSA, (b) rules (RL₇–RL₁₁) of LBSA, (c) rules (RL₁₂–RL₁₆) of LBSA, and (d) rules (RL₁₇–RL₁₉) of LBSA.

(a)
Rule label	Rule	Description
RL1	Nonce verification rule:	Principle P can decide that principle Q believes that X is fresh if P's Belief set contains $\#(X)$ and X from Q is in the P's possession set.
	$\frac{\#(X)\in \text{BEL}(P),X\hspace{0.17em}\hspace{0.17em}\text{from}\hspace{0.17em}\hspace{0.17em}Q\in \text{POSS}(P)}{\text{BEL}(P)=\text{BEL}(\mathrm{P})\cup \{\mathrm{Q}\text{\hspace{0.17em}believes}\hspace{0.17em}\#(X)\}}$
RL2	Message meaning rule:	P can believe that Q possesses X if it receives ${\left\{X\right\}}_k$ from Q and both P and Q know the key k.
	${\left\{X\right\}}_k$ from  $Q\in$ POSS $(P)$ ,
	$\frac{\left\{P,Q\right\}\subseteq \text{Observers}(k)}{\text{BEL}(P)=\text{BEL}(P)\cup \{X\in \text{POSS}(Q)\}}$
RL3	Sub-message freshness rule:  $\#(x_1)$ ∈ BEL $(P)$ ,	P can believe that $x_2$ is fresh if it believes that $x_1$ is fresh and have $x_1$ and $x_2$ in the same formula and this formula is in P's Possession set. That is, the part of the message that contains something fresh is fresh.
	$\frac{\left\{X\hspace{0.17em}\hspace{0.17em}\text{contains}\hspace{0.17em}{x}_{\mathrm{1}},X\hspace{0.17em}\text{contains}\hspace{0.17em}{x}_{\mathrm{2}}\right\}\subseteq \text{POSS}(P)}{\text{BEL}\left(P\right)=\text{BEL}(P)\cup \#(x_{\mathrm{2}})}$
RL4	Linkage rule (symmetric keys):	This rule is applied only once for the same nonce since the LINK item will be removed after applying it successfully. $P_i$ can believe that a submessage $x_1$ of a message X is fresh when several conditions are applied. The first one is when P's Belief set contains LINK (Na) which means the nonce Na has not been used before. Also, the message X that contains the nonce must be encrypted using the key k and k must be fresh and available to P; this is what other conditions state.
	#(k) ∈ BEL $(P),P\in$ Observers $(k)$ ,
	LINK(Na) ∈ BEL $(P)$ , X contains $f(Na)$ ,
	$\frac{X\hspace{0.17em}\text{contains}\hspace{0.17em}{x}_{\mathrm{1}},{\left\{X\right\}}_k\hspace{0.17em}\hspace{0.17em}\text{from}\hspace{0.17em}Q\in \text{POSS}(P)}{\text{BEL}\left(P\right)=\left(\text{BEL}\left(P\right)-\text{LINK}\left(Na\right)\right)\cup \{\#(x_{\mathrm{1}})\}}$
RL5	Linkage rules (asymmetric keys):	This rule is applied only once for the same nonce since the LINK item will be removed after applying it successfully. $P_i$ can believe that a submessage $x_1$ of a message X is fresh when several conditions are applied. The first one is when P's Belief set contains LINK (Na) which means the nonce Na has not been used before. Also, the message X that contains the nonce must be encrypted using the public key $k^{+}$ and the corresponding inverse (private) key $k^{-}$ must be fresh and available to P; this is what other conditions state.
	(a) $\#(k^{-})\in$ BEL(P), $P\in$ Observers $(k^{-})$ ,
	LINK(Na) ∈ BEL $(P)$ , X contains $f(Na)$ ,
	$\frac{X\hspace{0.17em}\text{contains}\hspace{0.17em}{x}_{\mathrm{1}},{\left\{X\right\}}_k^{+}\hspace{0.17em}\text{from\hspace{0.17em}}Q\in \text{POSS}(P)}{\text{BEL}(P)=(\text{BEL}(P)-\text{LINK}(Na))\cup \{\#(x_{\mathrm{1}})\}}$
	(b) $\#(k^{+})\in$ BEL(P), $P\in$ Observers $(k^{+})$ ,
	LINK(Na) ∈ BEL(P), X contains $f(Na)$ ,
	$\frac{X\hspace{0.17em}\text{contains}\hspace{0.17em}{x}_{\mathrm{1}},{\left\{X\right\}}_k^{-}\hspace{0.17em}\text{from\hspace{0.17em}}Q\in \text{POSS}(P)}{\text{BEL}(P)=(\text{BEL}(P)-\text{LINK\hspace{0.17em}}(Na))\cup \{\#(x_{\mathrm{1}})\}}$
RL6	Possible origins rule:	When P's possession set contains message X which contains submessage $x_1$ and this submessage observed by more than one principal, other than P, it will be marked as coming from all principals by adding new item for each of the P's Possession set.
	$X\in$ POSS(P), X contains $x_1$ ,
	$\frac{R\in \text{Observers}\left(x_{\mathrm{1}}\right),R\ne P}{x_{\mathrm{1}}\hspace{0.17em}\text{from\hspace{0.17em}\hspace{0.17em}}R\in \text{POSS}(P)}$

(b)
Rule label	Rule	Description
RL7	Submessage origin rule:	A submessage $x_2$ can be marked as coming from Q if P possesses a message X which contains $x_1$ and $x_2$ encrypted using an asymmetric key, and submessage $x_1$ is marked as coming from Q. And any other principle who observes the inverse key, the submessage is marked as coming from it.
	${\left\{X\right\}}_k^{+}$ ∈ POSS(P), Xcontains $x_1$ from Q,
	$\frac{R\in \text{Observers\hspace{0.17em}}(k^{-}),X\hspace{0.17em}\hspace{0.17em}\text{contains}\hspace{0.17em}{x}_{\mathrm{2}},R\ne P}{x_{\mathrm{2}}\hspace{0.17em}\text{from\hspace{0.17em}}Q\in \text{POSS}\left(P\right),x_{\mathrm{2}}\hspace{0.17em}\hspace{0.17em}\text{from}\hspace{0.17em}\hspace{0.17em}\hspace{0.17em}R\in \text{POSS}(P)}$
RL8	Submessage origin rule for asymmetric keys:	This rule is simplified version of the submessage origin rule. In (a) If P's Possession set contains message X which is encrypted using P's public key. And X contains a submessage $x_1$ which is marked as coming from Q. Then all other submessages in X are marked as coming from Q. This is true because P is the only principle that has the corresponding private key so no one can change the content of X. In (b) since Q is the constructor of the message X, any submessage of X can be marked as coming from Q. This is true because Q is the only principle that has Q's private key.
	(a) ${\left\{X\right\}}_{kp}^{+}\in$ POSS $(P)$ ,
	$\frac{X\hspace{0.17em}\text{contains}\hspace{0.17em}{x}_{\mathrm{1}}\hspace{0.17em}\hspace{0.17em}\text{from}\hspace{0.17em}Q,X\hspace{0.17em}\hspace{0.17em}\text{contains}\hspace{0.17em}{x}_{\mathrm{2}}}{x_{\mathrm{2}}\hspace{0.17em}\text{from\hspace{0.17em}}Q\in \text{POSS}(P)}$
	(b) Submessage origin rule for private keys:
	$\frac{{\left\{X\right\}}_{kQ}^{-}\in \text{POSS}(P),X\hspace{0.17em}\hspace{0.17em}\text{contains}\hspace{0.17em}{x}_{\mathrm{2}}}{x_{\mathrm{2}}\hspace{0.17em}\hspace{0.17em}\text{from}\hspace{0.17em}Q\in \text{POSS}(P)}$
RL9	Unbound key rule:	When key k is in P's Possession set and this key is not bounded to any principal then all principals (W) observe it. That is, the key is not a secret.
	$\frac{k\in \text{POSS\hspace{0.17em}}\left(P\right),\nexists Q:\left(k\bowtie Q\right)\in \text{POSS}(P)}{\text{Observers\hspace{0.17em}}(k)=W}$
RL10	Bound key origin rule for symmetric keys:	The protocol abort when P's Possession set contains the key k which is bound to principle Q, and $Q\ne P$ but this binding is not in P's bindings set which contains legal bindings for P.
	$(k\bowtie Q)\in$ POSS $(P),Q\ne P$ ,
	$\frac{\left(k\bowtie Q\right)\notin \text{Bindings}(P)}{\text{Abort}}$
RL11	Bound key origin rules for asymmetric keys:	If principle P has the binding of an asymmetric key to principle Q in its possession and binding sets and P's possession set contains a message that is encrypted under the inverse key this means that the message comes from Q because it is the only principle that have the inverse key. Otherwise, the protocol aborts.
	(a) ( $k^{+}\bowtie Q)\in$ POSS $(P)$ , $(k^{+}\bowtie Q)\notin$ Bindings(P)
	$\frac{{\left\{X\right\}}_k^{-}\hspace{0.17em}\hspace{0.17em}\text{from}\hspace{0.17em}R\in \text{POSS}(P),R\ne Q}{\text{Abort}}$
	(b) $(k^{-}\bowtie Q)\in$ POSS $(P)$ , $(k^{-}\bowtie Q)\notin$ Bindings $(P)$ ,
	$\frac{{\left\{X\right\}}_k^{+}\hspace{0.17em}\hspace{0.17em}\text{from}\hspace{0.17em}\hspace{0.17em}R\in \text{POSS}\left(P_{\mathrm{i}}\right),R\ne Q}{\text{Abort}}$

(c)
Rule label	Rule	Description
RL12	Conjunction rule:	When P's Proof set contains the proof that Q is accountable for the conjunction X and Y, then it will contain the proof that Q is accountable for X and Y, respectively. Contrariwise, the second one is used.
	(a) $\frac{\left(\mathrm{Q}\to \left(X,Y\right)\right)\in \text{Proofs}(P)}{\left(Q\to X\right)\in \text{Proofs}\left(P_i\right);\left(Q\to Y\right)\in \text{Proofs}(P)}$
	(b) $\frac{\left(Q\to X\right)\in \text{Proofs}\left(P\right);\left(Q\to Y\right)\in \text{Proofs}(P)}{\left(Q\to \left(X,Y\right)\right)\in \text{Proofs}(P)}$
RL13	Ciphertext understanding rule:	When P's Proof set contains the prove that Q is accountable for ${\left\{X\right\}}_k$ and Q holds k then it will contain the prove that Q is accountable for message X.
	( $Q\to {\left\{X\right\}}_k)\in$ Proofs $(P)$ ,
	$\frac{\left(k\in Q\right)\in \text{Proofs}(P)}{\left(Q\to X\right)\in \text{Proofs}(P)}$
RL14	Transfer rule:	When P's Proof set contains the proof that Trusted Third Party (TTP) is accountable for message X, then it will contain the proof that Q holds message X.
	$\frac{\left(\text{TTP}\to X\right)\in \text{Proofs}(P)}{\left(X\in Q\right)\in \text{Proofs}(P)}$
RL15	Timestamp rule (symmetric keys):	Timestamp rule defined to reason about the message.
	$\#(K)\in$ BEL $(P)$ , $K\in$ POSS $(P)$ ,
	$\#(T)\in$ BEL(P), X contains  $x_1$ ,
	$\frac{{\left\{X\right\}}_K\hspace{0.17em}\hspace{0.17em}\text{from\hspace{0.17em}}Q\in \text{POSS}(P)}{\text{BEL}\left(P\right)=\text{BEL}(P)\cup \{\#(x_1)\}}$
RL16	Timestamp rule (asymmetric keys):	Timestamp rule defined to reason about the message.
	$\#(K_Q^{+})\in$ BEL $(P)$ , $K_Q^{+}\in$ POSS $(P$ ),
	$\#(T)\in$ BEL $(P),\hspace{0.17em}\hspace{0.17em}X$ contains $x_1$ ,
	$\frac{{\left\{X\right\}}_{kQ}^{-}\hspace{0.17em}\text{from\hspace{0.17em}}Q\in \text{POSS}(P)}{\text{BEL}\left(P\right)=\text{BEL}(P)\cup \{\#(x_{\mathrm{1}})\}}$

(d)
Rule Label	Rule	Description
RL17	Authentication Rule:	This rule adds a new binding to the binding set. Note that its condition will not complete until the comparison action (ACT21) is executed successfully. Z could be any principle except P or TTP.
	( $K_Q^{+}\bowtie Q$ ) from $Z\in$ POSS $(P)$ ,
	$(K_Q^{+}\bowtie Q)\in$ BEL $(P)$ ,
	$\frac{{\left\{X\right\}}^{\mathrm{*}}\in \text{Proofs}(P)}{\text{Bindings}\left(P\right)=\text{Bindings}(P)\cup \{(K_Q^{+}\bowtie Q)\}}$
RL18	Integrity Rule:	This rule states that if ${\left\{X\right\}}^{*}\in$ Proof ( $P_i$ ) which means that X  received without any modification (i.e., as it sent from Q) then we add $X\in$   Poss (Q) to the believe set.
	$\frac{{\left\{X\right\}}^{\mathrm{*}}\in \text{Proof}(P)}{\text{BEL}\left(P\right)=\text{BEL}(P)\cup \{X\in \text{Poss}(Q)\}}$
RL19	Non-Repudiation Rule:	This rule states that if we have msg encrypted by $K_Q^{-}$   and the corresponding public key $K_Q^{+}$   in the Binding (P), we can prove that Q is responsible for sending message X.
	${\left\{X\right\}}_{kQ}^{-}\in$ Poss $(P)$ ,
	$\frac{\left(K_Q^{+}\bowtie Q\right)\in \text{Binding}(P),}{\left(Q\to X\right)\in \text{Proof}(P)}$

Section 5 provides mapping between security requirements and inference rules/actions. It also provides mapping between some protocol services and inference rules/actions.

5. Possible Mapping between Security Requirements and Inference Rules/Actions

To ensure that the required security requirement is achieved by a security protocol, some inference rules must be applied and some actions must be performed. In this section we provide possible mappings between each security requirement and the inference rule that must be applied or the action that must be executed to achieve it. Table 5 summarizes these mappings.

Table 5

Mappings between security requirements and Inference rules/actions.

Security Requirement	Inference Rules/Actions
Authentication	RL2, RL6, RL7, RL8, RL13, RL17
Authorization	ACT28
Confidentiality	ACT3, ACT4, ACT15
Integrity	${\text{RL}}_{\mathrm{18}}$
Non-Repudiation	RL2, RL6, RL7, RL8, RL13, RL19
Privacy	ACT3, ACT15
Availability	ACT13, ACT25, ACT26, ACT27, ACT28

Actions and rules are needed to complete the specification and the analysis processes. In other words, actions and rules add new values to the global and local sets which may result in achieving the mapped rules conditions.

Other actions and rules are needed to perform certain protocol services, including key management which deals with key and certificate generations, verification, and renewing. Certain services are related to nodes' interaction and protocol functions. Data item refreshments such as messages, keys, certificates, and nonces are among the data that need to be kept fresh.

Table 6 summarizes the mappings between protocol services and the inference rule that must be applied or the action that must be executed to achieve it.

Table 6

Mappings between protocol services and inference rules/actions.

Protocol Services	Inference rules/actions
Key management	ACT6, ACT11, ACT14, ACT16, ACT19, ACT22, ACT24, ACT30,
	RL4, RL5, RL9, RL10, RL11
Nodes interaction and protocol functions	ACT1, ACT2, ACT7, ACT8, ACT9, ACT12, ACT17, ACT18, ACT20, ACT21, ACT23, ACT29,
	RL12, RL14
Data refreshment	ACT5, ACT10,
	RL1, RL3, RL4, RL5, RL15, RL16

The following section presents how the above-presented architecture will be used to formally analyze security enforcers and security protocols.

6. Security Enforcers Specification and Analysis

Different security enforcers are used as part of different protocols to achieve security such as in [15–18]. In this section we have chosen well-known enforcers that can be provided at different network layers to illustrate how LBSA could be used to specify and analyze the security enforcers that could be used by many different security protocols. These enforcers are message authentication code (MAC) and digital certificate which also includes digital signature. The reason for using these enforcers is that they are the most used enforcers, in many protocols including routing protocols, to achieve authentication and integrity (MAC) and authentication, integrity and nonrepudiation (digital certificate) [19–25]. The following sections show how these enforcers could be verified using LBSA.

6.1. Message Authentication Code (MAC)

MAC [26] achieves two security requirements, namely, authentication and integrity. In MAC the sender and the receiver of the message must agree on a shared key before initiating the communication. The sender of the message uses the shared key and the message as an input to a hash function to generate the message digest. Then, the sender sends the message and the digest to the receiver. The receiver checks the originality of the message and its correctness by applying the hash function on the received message and the shared key. After that, the receiver compares the resulted digest with the received message digest. If the two digests are equal, this will prove the authenticity of the message as the shared key is only known by sender and receiver. Moreover, it ensures that the message is not modified during the transmission since any simple modification will produce a different digest. To mathematically prove that MAC achieves both authentication and integrity using LBSA the following steps must be performed.

(i) Define the Values of the Global Sets. The first step in the protocol specification is to define the values of the global sets:

•  

(GS1) $P=\{$ Alice, Bob} // Alice is assumed to be the initiator of the protocol.

 

(GS2) $R=$ {contains the rules defined in the Tables 4(a)–4(d)}

 

(GS3) $S=\{K_{\text{AB}}\}$ // $K_{\text{AB}}$   is the shared key between Alice and Bob

 

(GS4) Observers ( $K_{\text{AB}}$ ) $=\{\text{Alice}$ , Bob}.

(ii) Define the Initial Values of the Local Sets. The second step is to define the initial values of the local sets to each principal. Note that some of the global and the local sets values will be changed during the protocol analysis.

Principal A (Alice):

•  

(LS1) POSS(A) = {Msg, $K_{\text{AB}}$ , $(\text{B}\bowtie K_{\text{AB}})$ from B}

 

(LS2) BEL(A) = $\{\#(K_{\text{AB}}),(\text{B}\bowtie K_{\text{AB}})\}$

 

(LS6) BL =

•  

  (ACT₇) Concat $(\text{Msg},K_{\text{AB}})$

•  

  (ACT₁₂) Apply $(H,\{\text{Msg}.K_{\text{AB}}\})$ // Apply hash function to the concatenation

•  

  (ACT₇) Concat $(\text{Msg},H(\text{Msg}.K_{\text{AB}}))$ // prepare the message and digest

•  

  (ACT₁) Send $(\text{B},\{\text{Msg}.H(\text{Msg}.K_{\text{AB}})\})$ // send message and digest to B.

Principal B (Bob):

•  

(LS1) POSS(B) = $\{K_{\text{AB}},(\text{A}\bowtie K_{\text{AB}})\hspace{0.17em}\hspace{0.17em}\text{from}\hspace{0.17em}\text{A}\}$

 

(LS2) BEL(B) = $\{\#(K_{\text{AB}}),(\text{A}\bowtie K_{\text{AB}})\}$

 

(LS6) BL =

•  

  (ACT₂) Receive $(A,\{\text{Msg}.H(\text{Msg}.K_{\text{AB}})\})$

•  

  (ACT₈) Split $(\text{Msg}.H(\text{Msg.}{K}_{\text{AB}}))$

•  

  (ACT₇) Concat $(\text{Msg},K_{\text{AB}})$ // concatenate the received message with the key

•  

  (ACT₁₂) Apply $(H,\{\text{Msg}.K_{\text{AB}}\})$

•  

  (ACT₂₁) Comp $(H(\text{Msg}.K_{\text{AB}}),H(\text{Msg}.K_{\text{AB}}))$ // compare the calculated digest with the received one.

(iii) MAC Analysis. The last step is to analyze the security enforcer which is MAC in this case to check security requirements it achieves.

Alice is assumed to be the initiator of the protocol. Therefore, four actions in the BL(A) are executed which add new values to the POSS(A) set:

$$\begin{array}{l}\text{POSS}\left(\text{A}\right)=\{\text{Msg},K_{\text{AB}},\left(\text{B}\bowtie K_{\text{AB}}\right)\mathrm{\hspace{0.17em}\hspace{0.17em}}\text{from}\mathrm{\hspace{0.17em}\hspace{0.17em}}\text{B},\mathrm{\hspace{0.17em}\hspace{0.17em}}\\ \hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{0.17em}\hspace{0.17em}\left\{\text{Msg}.K_{\text{AB}}\right\},H\left(\text{Msg}.K_{\text{AB}}\right)\}.\end{array}$$

(1)

So far no inference rules can be applied. Now, actions in BL(B) are executed and this will produce new values that are added to POSS(B) and the Proof(B) sets. Consequently, both integrity and authentication inference rules can be applied:

$$\begin{array}{l}\text{POSS}\left(\text{B}\right)=\{K_{\text{AB}},\left(\text{A}\bowtie K_{\text{AB}}\right)\hspace{0.17em}\hspace{0.17em}\text{from}\mathrm{\hspace{0.17em}\hspace{0.17em}}\text{A},\text{Msg},\mathrm{\hspace{0.17em}\hspace{0.17em}}\mathrm{\hspace{0.17em}\hspace{0.17em}}\\ \hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{0.17em}\hspace{0.17em}H\left(\text{Msg}.K_{\text{AB}}\right),\left\{\text{Msg}.K_{\text{AB}}\right\},H\left(\text{Msg}.K_{\text{AB}}\right)\}\\ \hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\hspace{1em}\text{Proof}\left(\text{B}\right)=\left\{{\left\{\text{Msg}\right\}}^{*}\right\}.\end{array}$$

(2)

Since ${\{\text{Msg}\}}^{*}\in \text{Proof}(\text{B})$ , we can apply the authentication rule ( $RL17$ ) and the integrity rule ( $RL18$ ) as follows.

Authentication Rule (RL17):

$$\begin{array}{cc}& \frac{\left(\text{A}\bowtie K_{\text{AB}}\right)\mathrm{\hspace{0.17em}\hspace{0.17em}}\text{from}\mathrm{\hspace{0.17em}\hspace{0.17em}}\text{A}\in \text{POSS}\left(\text{B}\right)}{\text{Binding}\left(\text{B}\right)=\text{Binding}\left(\text{B}\right)\cup \left\{\left(\text{A}\bowtie K_{\text{AB}}\right)\right\}}\\ \frac{\left(\text{A}\bowtie K_{\text{AB}}\right)\in \text{BEL}\left(\text{B}\right),{\left\{\text{Msg}\right\}}^{*}\in \text{Proof}\left(\text{B}\right)}{\text{Binding}\left(\text{B}\right)=\text{Binding}\left(B\right)\cup \left\{\left(\text{A}\bowtie K_{\text{AB}}\right)\right\}}.\end{array}$$

(3)

By applying the authentication rule, we proved that MAC successfully authenticated the sender. Since the result of comparison ends successfully, the binding of the shared key and the identity of sender (Alice in this scenario) will be added to the binding set of Bob which ensures the authenticity of the received message.

Integrity Rule (RL18):

$$\begin{array}{cc}& \frac{{\left\{\text{Msg}\right\}}^{*}\in \text{Proof}\left(\text{B}\right)}{\text{BEL}\left(\text{B}\right)=\text{BEL}\left(\text{B}\right)\cup \left\{\text{Msg}\in \text{POSS}\left(\text{A}\right)\right\}}.\end{array}$$

(4)

The equality of the two digests also proves the correctness of the received message which leads Bob to adding a new value to Bob's Belief set indicating that the received message is the same as the message sent by Alice.

As can be concluded, LBSA has been used to mathematically prove the achievement of authentication and integrity by MAC. The above process is also applicable to any other security enforcer.

6.2. Digital Certificate

In hierarchical trust model, digital certificate [14] is usually issued by a certification authority (CA). It contains the user identity, public key ( $K^{+}$ ), CA's digital signature, and other information. Using the CA's digital signature, the user can proof the authenticity of the issuer and ensure correct binding between the identity and the public key in the certificate.

We assume that the CA is the initiator of the protocol which will make one certificate for Alice and another for Bob. It sends each certificate after attaching its signature. Bob needs Alice's public key to send messages to her securely, therefore Alice sends her certificate to Bob then Bob starts the signature verification to ensure correct binding between Alice's public key and her identity.

Using LBSA to prove the achieved security requirements using the digital certificate, we start by presenting the enforcer specification in terms of global and local sets and then we performed the analysis part.

(i) Define the Values of the Global Sets.  Consider

•  

(GS1) $P=\{\text{CA, Alice, Bob}\}$

 

(GS2) $R=\{$ contains the rules defined in Tables 4(a)–4(d)}

 

(GS3) $S=\{K_{\text{CA}}^{-},K_{\text{A}}^{-},K_{\text{B}}^{-}\}$

 

(GS4) Observers ( $K_{\text{CA}}^{-}$ ) = $\{\text{CA}\}$

 

(GS4) Observers ( $K_{\text{A}}^{-}$ ) = $\{\text{A}\}$

 

(GS4) Observers ( $K_{\text{B}}^{-}$ ) = $\{\text{B}\}$ .

(ii) Define the Initial Values of the Local Sets to each Principal

Principal (CA):

•  

(LS1) POSS(CA) = $\{K_{\text{CA}}^{-},K_{\text{CA}}^{+}\}$

 

(LS2) BEL(CA) = $\{\#(K_{\text{CA}}^{-}),\#(K_{\text{CA}}^{+})\}$

 

(LS7) Binding(CA) = $\{\text{CA}\bowtie K_{\text{CA}}^{+}\}$

 

(LS6) BL =

•  

  // Generation of Alice's certificate

•  

  (ACT₁₂) Apply $(H,\text{cer}{\text{t}}_{\text{A}})$ // digest generation

•  

  (ACT₁₅) Apply-asymkey $(H({\text{cert}}_{\text{A}})$ , $K_{\text{CA}}^{-}$ ) // generation of CA's digital signature

•  

  (ACT₇) Concat $({\text{cert}}_{\text{A}}$ , ${\{H({\text{cert}}_{\text{A}})\}}_{K_{\text{CA}}^{-}})$

•  

  (ACT₁) Send $(\text{Alice},{\text{cert}}_{\text{A}}.{\{H({\text{cert}}_{\text{A}})\}}_{K_{\text{CA}}^{-}})$

•  

  // Generation of Bob's certificate

•  

  (ACT₁₂) Apply $(H,{\text{cert}}_{\text{B}})$

•  

  (ACT₁₅) Apply-asymkey $(H$ (cert_B), $K_{\text{CA}}^{-}$ )

•  

  (ACT₇) Concat(cert_B, ${\{H({\text{cert}}_{\text{B}})\}}_{K_{\text{CA}}^{-}})$

•  

  (ACT₁) Send $($ Bob, ${\text{cert}}_{\text{B}}.{\{H({\text{cert}}_{\text{B}})\}}_{K_{\text{CA}}^{-}})$ .

Principal (A) (Alice):

•  

(LS1) POSS $($ A $)=\{K_{\text{A}}^{-},K_{\text{A}}^{+},K_{\text{CA}}^{+}\}$

 

(LS2) BEL $($ A $)=\{\#(K_{\text{A}}^{-}),\#(K_{\text{A}}^{+}),\#(K_{\text{CA}}^{+})\}$

 

(LS7) Binding $(\text{CA})=\{\text{A}\bowtie K_{\text{A}}^{+},\text{CA}\bowtie K_{\text{CA}}^{+}\}$

 

(LS6) BL =

•  

  (ACT₂) Receive (CA, ${\text{cert}}_{\text{A}}.{\{H({\text{cert}}_{\text{A}})\}}_{K_{\text{CA}}^{-}})$

•  

  (ACT₁) Send (Bob, ${\text{cert}}_{\text{A}}.{\{H(\text{cer}{\text{t}}_{\text{A}})\}}_{K_{\text{CA}}^{-}}$ )—A(1).

Principal ( B ) (Bob):

•  

(LS1) POSS(B) $=\{K_{\text{B}}^{-},K_{\text{B}}^{+},K_{\text{CA}}^{+}\}$

 

(LS2) BEL(B) $=\{\#(K_{\text{B}}^{-}),\#(K_{\text{B}}^{+}),\#(K_{\text{CA}}^{+})\}$

 

(LS7) Binding(B) $=\{\text{B}\bowtie K_{\text{B}}^{+},\text{CA}\bowtie K_{\text{CA}}^{+}\}$

 

(LS6) BL =

•  

  (ACT₂) Receive $(\text{CA},{\text{cert}}_{\text{B}}$ . $\hspace{0.17em}{\{H({\text{cert}}_{\text{B}})\}}_{K_{\text{CA}}^{-}}$ ) // Bob receives its certificate from the CA

•  

  (ACT₂) Receive(Alice, $\text{cer}{\text{t}}_{\text{A}}$ . ${\{H(\text{cer}{\text{t}}_{\text{A}})\}}_{K_{\text{CA}}^{-}})$ // Bob receives Alice's certificate from the Alice—B(1)

•  

  (ACT₈) Split $(\text{cer}{\text{t}}_{\text{A}}.{\{H(\text{cer}{\text{t}}_{\text{A}})\}}_{K_{\text{CA}}^{-}})$ —B(2)

•  

  (ACT₂₁) Comp $(\text{Apply}(H,\text{cer}{\text{t}}_{\text{A}})$ , Apply-asymkey $({\{H(\text{cer}{\text{t}}_{\text{A}})\}}_{K_{\text{CA}}^{-}},K_{\text{CA}}^{+}))$

•  

  // Bob compares the calculated digest and the digest resulted from the decryption of the digital signature—B(3).

(iii) Digital Certificate Analysis. CA is assumed to be the initiator of the protocol and the first four actions in the BL(CA) are executed which will add new values to the POSS(CA) as follows:

•  

POSS(CA) $=\{K_{\text{CA}}^{-},K_{\text{CA}}^{+}$ , $H(\text{cer}{\text{t}}_{\text{A}})$ , ${\{H({\text{cert}}_{\text{A}})\}}_{K_{\text{CA}}^{-}}$ , cert_A. ${\{H({\text{cert}}_{\text{A}})\}}_{K_{\text{CA}}^{-}}\}$ .

The next action to be executed is the first action in BL(A) which will receive the msg and update the POSS(A) to include the msg content:

•  

POSS(A) = $\{K_{\text{A}}^{-},K_{\text{A}}^{+}$ , $K_{\text{CA}}^{+},\text{cer}{\text{t}}_{\text{A}}.{\{H(\text{cer}{\text{t}}_{\text{A}})\}}_{K_{\text{CA}}^{-}}\}$ . Then CA does the rest of the actions which followed by executing the first action in BL(B) and these actions update the POSS(CA) again and the POSS(B).

 

POSS(CA) = $\{K_{\text{CA}}^{-}$ , $K_{\text{CA}}^{+}$ , H( $\text{cer}{\text{t}}_{\text{A}}$ ), ${\{H(\text{cer}{\text{t}}_{\text{A}})\}}_{K_{\text{CA}}^{-}}$ , $\text{cer}{\text{t}}_{\text{A}}.{\{H(\text{cer}{\text{t}}_{\text{A}})\}}_{K_{\text{CA}}^{-}}$ , H(cert_B), ${\{H(\text{cer}{\text{t}}_{\text{B}})\}}_{K_{\text{CA}}^{-}}$ , $\text{cer}{\text{t}}_{\text{B}}.{\{H(\text{cer}{\text{t}}_{\text{B}})\}}_{K_{\text{CA}}^{-}}\}$ .

 

POSS(B) = $\{K_{\text{B}}^{-},K_{\text{B}}^{+},K_{\text{CA}}^{+},{\text{cert}}_{\text{B}}.{\{H({\text{cert}}_{\text{B}})\}}_{K_{\text{CA}}^{-}}\}$ .

Now Alice sends her certificate to Bob which is the action A(1) in the BL(A) and the next actions to be executed are B(1)-B(2) which update the POSS(B):

•  

POSS(B) = $\{K_{\text{B}}^{-},K_{\text{B}}^{+},K_{\text{CA}}^{+}$ , ${\text{cert}}_{\text{B}}.{\{H({\text{cert}}_{\text{B}})\}}_{K_{\text{CA}}^{-}}$ , ${\text{cert}}_{\text{A}}.{\{H({\text{cert}}_{\text{A}})\}}_{K_{\text{CA}}^{-}}$ , cert_A, ${\{H({\text{cert}}_{\text{A}})\}}_{K_{\text{CA}}^{-}}\}$ .

Since ${\text{cert}}_{\text{A}}.{\{H({\text{cert}}_{\text{A}})\}}_{K_{\text{CA}}^{-}}\in \text{POSS}(\text{B})$ we can apply Submessage origin rule (RL7):

$$\begin{array}{cc}& \frac{{\text{cert}}_{\text{A}}.{\left\{H\left({\text{cert}}_{\text{A}}\right)\right\}}_{K_{\text{CA}}^{-}}\in \text{POSS}\left(\text{B}\right)}{(K_{\text{A}}^{+}\bowtie \text{A})\hspace{0.17em}\hspace{0.17em}\text{from}\hspace{0.17em}\hspace{0.17em}\text{CA}\in \text{POSS}\left(\text{B}\right)},\\ \frac{{\text{cert}}_{\text{A}}.{\left\{H\left({\text{cert}}_{\text{A}}\right)\right\}}_{K_{\text{CA}}^{-}}\text{contains}\hspace{0.17em}\hspace{0.17em}{K}_{\text{A}}^{+}}{(K_{\text{A}}^{+}\bowtie \text{A})\hspace{0.17em}\hspace{0.17em}\text{from}\hspace{0.17em}\hspace{0.17em}\text{CA}\in \text{POSS}\left(\text{B}\right)}.\end{array}$$

(5)

Which adding a new value to the POSS(B):

•  

$\text{POSS}(\text{B})=\{K_{\text{B}}^{-},K_{\text{B}}^{+},K_{\text{CA}}^{+},{\text{cert}}_{\text{B}}.{\{H({\text{cert}}_{\text{B}})\}}_{K_{\text{CA}}^{-}}$ , ${\text{cert}}_{\text{A}}.{\{H({\text{cert}}_{\text{A}})\}}_{K_{\text{CA}}^{-}}$ , cert_A, ${\{H({\text{cert}}_{\text{A}})\}}_{K_{\text{CA}}^{-}}$ , ( $K_{\text{A}}^{+}\bowtie \text{A}$ ) from CA}.

Finally, executing the action B(3) will add new values to POSS(B) (assuming the comparison action ensures equality) which achieves some rules conditions and these rules can be applied:

•  

POSS(B) = $\{K_{\text{B}}^{-},K_{\text{B}}^{+}$ , $K_{\text{CA}}^{+}$ , cert_B. ${\{H({\text{cert}}_{\text{B}})\}}_{K_{\text{CA}}^{-}}$ , $\text{cer}{\text{t}}_{\text{A}}$ . ${\{H({\text{cert}}_{\text{A}})\}}_{K_{\text{CA}}^{-}}$ , ${\text{cert}}_{\text{A}}.{\{H({\text{cert}}_{\text{A}})\}}_{K_{\text{CA}}^{-}}$ , ( $K_{\text{A}}^{+}\bowtie$ A) from CA, $H({\text{cert}}_{\text{A}})$ , $H({\text{cert}}_{\text{A}})$ , ${\{{\text{cert}}_{\text{A}}\}}^{*}\}$ .

Since ( $K_{\text{A}}^{+}\bowtie \text{A}$ ) from CA ∈ POSS(B), ${\{{\text{cert}}_{\text{A}}\}}^{*}\in$ POSS(B) we can apply authentication and integrity rules as follows.

Authentication Rule (RL17):

$$\begin{array}{cc}& \frac{\left(K_{\text{A}}^{+}\bowtie \text{A}\right)\hspace{0.17em}\hspace{0.17em}\text{from}\hspace{0.17em}\hspace{0.17em}\text{CA}\in \text{POSS}\left(\text{B}\right)}{\text{Binding}\left(\text{B}\right)=\text{Binding}\left(\text{B}\right)\cup \left\{\left(K_{\text{A}}^{+}\bowtie \text{A}\right)\right\}},\\ \frac{\mathrm{\hspace{0.17em}\hspace{0.17em}}\left(K_{\text{CA}}^{+}\bowtie \text{A}\right)\in \text{BEL}\left(\text{B}\right),{\left\{{\text{cert}}_{\text{A}}\right\}}^{*}\in \text{Proof}\left(\text{B}\right)}{\text{Binding}\left(\text{B}\right)=\text{Binding}\left(\text{B}\right)\cup \left\{\left(K_{\text{A}}^{+}\bowtie \text{A}\right)\right\}}.\end{array}$$

(6)

Integrity Rule (RL18):

$$\begin{array}{cc}& \frac{{\left\{{\text{cert}}_{\text{A}}\right\}}^{*}\in \text{Proof}\left(\text{B}\right)}{\text{BEL}\left(\text{B}\right)=\text{BEL}\left(\text{B}\right)\cup \left\{{\text{cert}}_{\text{A}}\in \mathrm{\hspace{0.17em}\hspace{0.17em}}\text{Poss}\left(\text{A}\right)\right\}}.\end{array}$$

(7)

Nonrepudiation Rule (RL19):

$$\begin{array}{cc}& \frac{{\left\{H\left({\text{cert}}_{\text{A}}\right)\right\}}_{K_{\text{CA}}^{-}}\in \text{Poss}\left(\text{B}\right),\left(K_{\text{CA}}^{+}\bowtie \text{CA}\right)\in \text{Binding}\left(\text{B}\right)}{\left(\text{CA}\to {\text{cert}}_{\text{A}}\right)\in \text{Proof}\left(\text{B}\right)}.\end{array}$$

(8)

Consequently, applying Authentication Rule (RL17) ensures the authenticity of Alice's public key. Integrity Rule (RL18) confirms the correctness of Alice's certificate. Finally, Nonrepudiation Rule (RL19) proves the originality of Alice's certificate, in other words it proves that Alice's certificate was issued and signed by the CA.

The purpose of LBSA is to generalize the rules, but the way they are applied depends on the enforcer itself. As shown this section, Rules 17 and 18 are used by both MAC and digital certificates but in different meanings. The authentication rule in MAC ensures the authenticity of the received message, whereas in digital certificate it ensures the authenticity of the public key. The integrity rule is used in MAC to ensure the correctness of the received message whereas in digital certificate it used to ensure the correctness of the certificate's contents.

7. Case Study: Ariadne Protocol

Many secure routing protocols have been proposed in the literature [27–32]. In this section, Ariadne protocol [27], which is a secure, on-demand routing protocol for multihop wireless networks was chosen to illustrate how to use LBSA to specify and analyze secure protocols. Ariadne is based on Timed Efficient Stream Loss-tolerant Authentication (TESLA) [33] which is an efficient broadcast authentication scheme that requires time synchronization. TESLA is commonly used in wireless sensor networks due to its low communication and computation overhead.

Before we start the security verification of Ariadne, we will present an overview of Ariadne route discovery using TESLA. For simplicity, we will use four nodes but what is applied in case of four nodes can be applied to more nodes. In all cases we will have a source, a destination, and a set of intermediate nodes which their number can vary depending on the chosen route. In the case of using more nodes, the change will be in the length of the chain of nodes. The way the authentication and integrity are achieved is defined by the Ariadne protocol itself. In this case study, we mapped Ariadne to LBSA to check Ariadne security correctness.

The source node S begins route instantiation to destination D by broadcasting a route request packet. A and B are intermediate nodes, that is, S → A → B → D. A route reply packet is unicasted by the destination D as a reply to the request packet along the reverse path to the source.

In the route discovery process there are two types of messages REQUEST and REPLY. REQUEST and REPLY messages include the following fields.

Route REQUEST packet in Ariadne contains eight fields: REQUEST (define the type of the message), initiator address, target address, id (uniquely identifies the request), time interval, hash chain, node list, and MAC list. Note that the last three fields are updated by each intermediate node receiving that request.

Table 7 shows the protocol parameters.

Table 7

Ariadne protocol parameters.

Parameter name	Meaning
$S\mathrm{\hspace{0.17em}\hspace{0.17em}}$	Initiator (source) node.
D	Target (destination) node.
$K_{SD}$ , $K_{DS}$	shared secret keys between S and D for message authentication in each direction.
$t_i$	Time interval.
Id	Message identifier.
$K_{A\text{ti}}$	TESTLA key (K) used by principal (A), i is the index for the time interval specified in the request.
$K_{B\text{ti}}$	TESTLA key (K) used by principal (B), i is the index for the time interval specified in the request.

The following steps illustrate how Ariadne route discovery using TESLA works:

•  

S: $h_0={\text{MAC}}_{KSD}$ (REQUEST, S, D, id, ti)

 

S→ broadcast: (REQUEST, S, D, id, ti, $h_0$ , ( ), ( ))

 

A: $h1$ = H(A, $h_0$ )

 

$M_A={\text{MAC}}_{KA\text{ti}}$ (REQUEST, S, D, id, ti, $h1$ , (A), ( ))

 

$A\to$ broadcast: (REQUEST, S, D, id, ti, $h1$ , (A), ( $M_A$ ))

 

B: h2= H(B, h1)

 

$M_B={\text{MAC}}_{KB\text{ti}}$ (REQUEST, S, D, id, ti, $h1$ , ( $A,B$ ), ( $M_A$ ))

 

$B\to$ broadcast: (REQUEST, S, D, id, ti, $h2$ , ( $A,B$ ), ( $M_A$ , $M_B$ ))

 

D: $M_D={\text{MAC}}_{KSD}$ (REPLY, D, S, ti, ( $A,B$ ), ( $M_A$ , $M_B$ ))

 

$D\to$ B: (REPLY, D, S, ti, ( $A,B$ ), ( $M_A$ , $M_B$ ), $M_D$ , ( ))

 

$B\to$ A: (REPLY, D, S, ti, ( $A,B$ ), ( $M_A$ , $M_B$ ), $M_D$ , ( $K_{B\text{ti}}$ ))

 

$A\to$ S: (REPLY, D, S, ti, ( $A,B$ ), ( $M_A,M_B$ ), $M_D$ , ( $K_{B\text{ti}},K_{A\text{ti}})$ ).

In the Ariadne protocol, the initiator of the REQUEST initializes the hash chain ( $h_0$ ) to ${\text{MAC}}_{KSD}$ (initiator, target, id, time interval) and the node list and MAC list to empty lists.

When any node A receives a route REQUEST for which it is not the target, the node checks its local table of (initiator, id) values from recent REQUESTs it has received to determine if it has already seen a REQUEST from this same Route Discovery. If it has, the node discards the packet. The node also checks whether the time interval in the REQUEST is valid. Then, the node modifies the REQUEST by appending its own address, A, to the node list in the REQUEST, replacing the hash chain field with H (A, hash chain), and appending a MAC of the entire REQUEST to the MAC list. The node uses the TESLA key $K_{A\text{ti}}$ to compute the MAC, where i is the index for the time interval specified in the REQUEST. Then, the node rebroadcast the modified REQUEST.

If the target node (destination) determines that the REQUEST is valid, it returns a route REPLY to the initiator, containing eight fields: REPLY (define the type of the message), target address (which is the initiator address in the REQUEST message), initiator address (which is the target address in the REQUEST message), time interval (the same as in the REQUEST message), node list, MAC list, target MAC, and key list. The target MAC is set to a MAC computed on the preceding fields in the REPLY with the key $K_{DS}$ , and the key list is initialized to the empty list. The route REPLY is then returned to the initiator of the REQUEST along the source route obtained by reversing the sequence of hops in the node list of the REQUEST.

7.1. Ariadne Specification

First we will present the assumptions of Ariadne protocol which are as follows.

• (i)

The source S and destination D share the MAC keys $K_{SD}$ and $K_{DS}$ .

(ii)

Every node has a TESLA one-way key chain.

(iii)

All nodes know the authentication key of TESLA one-way key chain of each other node.

(i) Define the Values of the Global Sets. Consider

•  

(GS1) $P=\{S,A,B,D\}$

 

(GS2) $R=\{$ contains the rules defined in Tables 4(a)–4(d)}

 

(GS3) $S=\{K_{SD},K_{DS},K_{B\text{ti}},K_{A\text{ti}}\}$

 

(GS4) Observers $\mathrm{\hspace{0.17em}\hspace{0.17em}}(K_{SD})=\{S,D\}$

 

(GS4) Observers $(K_{A\text{ti}})=\{A,S\}$

 

(GS4) Observers $(K_{B\text{ti}})=\{B,S\}$

 

(GS4) Observers $(K_{DS})=\{D,S\}$ .

(ii) Define the Initial Values of the Local Sets for each Principal

Principal ( S ):

•  

(LS1) POSS $(S)=\{K_{DS},K_{SD},K_{A\text{ti}},K_{B\text{ti}}$ , $(D\bowtie K_{DS})$ from D, $(D\bowtie K_{SD})$ from D, ( $A\bowtie K_{A\text{ti}}$ ) from A, $(B\bowtie K_{B\text{ti}})$ from $B\}$

 

(LS2) BEL $(S)=\{\#(K_{DS}),\#(K_{SD}),\#(K_{A\text{ti}}),\#(K_{B\text{ti}})$ , $(D\bowtie K_{DS})$ , $(D\bowtie K_{SD})$ , $(A\bowtie K_{A\text{ti}})$ , $(B\bowtie K_{B\text{ti}})\}$

 

(LS6) BL =

•  

  (ACT₇) Concat ({REQUEST, S, D, id, ti}, $K_{SD}$ )—S(1)

•  

  (ACT₁₂, ACT₂₉) $h_0\leftarrow$ Apply $(H,\{$ REQUEST, $S,D$ , id, ti}. $K_{SD}$ )—S(2)

•  

  (ACT₁₈) Broadcast ({REQUEST, $S,D$ , id, ti, $h_0$ , (), () })—S(3)

•  

  (ACT₂) Receive (A, {REPLY, $D,S$ , ti, $(A,B)$ , ( $M_A,M_B$ ), $M_D$ , $(K_{B\text{ti}},K_{A\text{ti}})\})$ —S(4)

•  

  (ACT₇) Concat({REPLY, $D,S$ , id, ti, ( $A,B$ ), ( $M_A$ , $M_B$ )}, $K_{DS}$ )—S(5)

•  

  (ACT₁₂, ACT₂₉) $C1\leftarrow$ Apply $(H$ , {REPLY, $D,S$ , id, ti, ( $A,B$ ), $(M_A,M_B)\}.K_{DS})$ —S(6)

•  

  (ACT₂₁) Comp $(M_D,C1)$ —S(7)

•  

  (ACT₇) Concat $(\{$ REQUEST, $S,D$ , id, ti, $h1$ , (A), $()\},A_{\text{ti}})$ —S(8)

•  

  (ACT₁₂, ACT₂₉) $C2\leftarrow$ Apply $(H$ ,{REQUEST, $S,D$ , id, ti, $h1$ , (A), $()\}.A_{\text{ti}})$ —S(9)

•  

  (ACT₂₁) Comp $(M_A,C2$ )—S(10)

•  

  (ACT₇) Concat $(\{$ REQUEST, $S,D$ , id, ti, $h2$ , ( $A,B$ ), $()\},B_{\text{ti}})$ —S(11)

•  

  (ACT₁₂, ACT₂₉) $C3\leftarrow$ Apply(H, {REQUEST, $S,D$ , id, ti, $h2$ , ( $A,B$ ), $()\}.B_{\text{ti}})$ —S(12)

•  

  (ACT₂₁) Comp $(M_B,C3)$ —S(13).

Principal (A):

•  

(LS1) POSS $(A)=\{A_{\text{ti}}\}$

 

(LS2) BEL $(A)=\{\#(A_{\text{ti}})\}$

 

(LS7) Binding $(A)=\{A_{\text{ti}}\bowtie \text{ti}\}$

 

(LS6) BL =

•  

  (ACT₂) Receive({REQUEST, $S,D$ , id, ti, $h_0$ , $(),()\})$ —A(1)

•  

  (ACT₂₀) Check-request(S, id)—A(2)

•  

  (ACT₁₀) Check-freshness(ti)—A(3)

•  

  (ACT₇) Concat(A, $h_0$ )—A(4)

•  

  (ACT₁₂, ACT₂₉) $h1\leftarrow$ Apply $(H,\{A.h_0\})$ —A(5)

•  

  (ACT₇) Concat $(\{$ REQUEST, $S,D$ , id, ti, $h1$ , $(A),()\}$ , $A_{\text{ti}})$ —A(6)

•  

  (ACT₁₂, ACT₂₉) $M_A\leftarrow$ Apply $(H$ , {REQUEST, $S,D$ , id, ti, $h1$ , (A), $()\}.A_{\text{ti}})$ —A(7)

•  

  (ACT₁₈) Broadcast $(\{$ REQUEST, $S,D$ , id, ti, $h1$ , ( $A),(M_A)\}$ —A(8)

•  

  (ACT₂) Receive(B,{REPLY, $D,S$ , ti, $(A,B)$ , $(M_A,M_B)$ , $M_D,(K_{B\text{ti}})\})$ —A(9)

•  

  (ACT₁) Send(S, {REPLY, $D,S$ , ti, ( $A,B$ ), $(M_A,M_B),M_D,(K_{B\text{ti}},K_{A\text{ti}})\})$ —A(10).

Principal ( B ):

•  

(LS1) POSS $(B)=\{B_{\text{ti}}\}$

 

(LS2) BEL $(B)=\{\#(B_{\text{ti}})\}$

 

(LS7) Binding $(B)=\{B_{\text{ti}}\bowtie \text{ti}\}$

 

(LS6) BL =

•  

  (ACT₂) Receive({REQUEST, $S,D$ , id, ti, $h1$ , (A), $(M_A)\})$ — B(1)

•  

  (ACT₂₀) Check-request(S, id)— B(2)

•  

  (ACT₁₀) Check-freshness(ti)— B(3)

•  

  (ACT₇) Concat( $B,h1$ )— B(4)

•  

  (ACT₁₂, ACT₂₉) $h2\leftarrow$ Apply( $H,\{B.h1\}$ )— B(5)

•  

  (ACT₇) Concat({REQUEST, $S,D$ , id, ti, $h2$ , ( $A,B),()\},B_{\text{ti}})$ —B(6)

•  

  (ACT₁₂, ACT₂₉) $M_B\leftarrow$ Apply $(H,\{$ REQUEST, $S,D$ , id, ti, $h2$ , ( $A,B$ ), $()\}.B_{\text{ti}})$ —B(7)

•  

  (ACT₁₈) Broadcast $(\{$ REQUEST, $S,D$ , id, ti, $h2$ , ( $A,B$ ), $(M_A,M_B)\}$ —B(8)

•  

  (ACT₂) Receive $(D,\{$ REPLY, $D,S$ , ti, ( $A,B$ ), ( $M_A,M_B$ ), $M_D$ , $()\})$ —B(9)

•  

  (ACT₁) Send $(A,\{$ REPLY, $D,S$ , ti, ( $A,B$ ), $(M_A,M_B),M_D,(K_{B\text{ti}})\}$ — B(10).

Principal (D):

•  

(LS1) POSS $(D)=\{K_{DS},K_{SD}$ , $(S\bowtie K_{SD})$ from S, $(S\bowtie K_{DS})$ from $S\}$

 

(LS2) BEL $(D)=\{\#(K_{SD})$ , $\#(K_{SD})$ , $K_{SD}\bowtie S$ , $K_{DS}\bowtie S\}$

 

(LS6) BL =

•  

  (ACT₂) Receive $(\{$ REQUEST, $S,D$ , id, ti, $h2$ , ( $A,B$ ), $(M_A,M_B)\}$ —D(1)

•  

  (ACT₂₀) Check-request(S, id)—D(2)

•  

  (ACT₁₀) Check-freshness(ti)—D(3)

•  

  (ACT₁₂, ACT₂₉) $\text{C}\mathrm{1}\leftarrow$ Apply(H, Concat(A, Apply(H, Concat (B, Apply(H, (ACT₇) Concat $(\{$ REQUEST, S, D, id, ti $\},K_{SD}))))))$ —D(4)

•  

  (ACT₂₁) Comp $(h2,C1)$ —D(5)

•  

  (ACT₇) Concat $(\{$ REPLY, D, S, id, ti, ( $A,B$ ), $(M_A,M_B)\},K_{DS})$ —D(6)

•  

  (ACT₁₂, ACT₂₉) $M_D\leftarrow$ Apply $(H,\{$ REPLY, D, S, id, ti, $(A,B)$ , $(M_A,M_B)\}$ . $K_{\text{DS}})$ —D(7)

•  

  (ACT₁) Send $(B,\{$ REPLY, D, S, ti, $(A,B),(M_A,M_B),M_D,()\})$ —D(8).

7.2. Ariadne Analysis

Node S is the initiator of the protocol and its first three actions will be executed which result in new values to be added to the POSS(S) set:

•  

POSS(S):= POSS(S) $\cup (\{\{\text{REQUEST},S,D$ , id, ti $\}.K_{SD}\}$ , $\{h_0=H(\{$ REQUEST, $S,D$ , id, ti $\}.K_{SD})\})$ .

Now we assume that node A receives the request so first eight actions in BL(A) will be executed and the result is

•  

POSS(A) = POSS(A) $\cup \{\{\text{REQUEST},S,D,\text{id},\text{ti}$ , $h_{\mathrm{0}},(),()\},A.h_0,h\mathrm{1}=H(A.h_0)$ ,

 

$M_A$ = $H(\{$ REQUEST, $S,D$ , id, ti $,h\mathrm{1},(A),()\}.A_{\text{ti}})\}$

 

BEL(A) = $\text{BEL}(A)\cup \{\#(\text{ti})\}$ .

Now B(1–8) will be executed and the result is

•  

POSS $(B)=$ POSS(B) $\cup \{\{\text{REQUEST},S,D,\text{id},\text{ti},h\mathrm{1}$ , (A), ( $M_A)\}$ , $B.h\mathrm{1},h\mathrm{2}=$ $H(B.h\mathrm{1})$ , {REQUEST, $S,D$ , id, ti, $h\mathrm{2},(A,B),()\}.B_{\text{ti}}$ , $M_B=H(\{$ REQUEST, $S,D$ , id, ti, $h\mathrm{2},(A,B),()\}.B_{\text{ti}})\}$

 

BEL $(B)=$ BEL $(B)\cup \{\#(\text{ti})\}$ .

Now the request reaches its target which is node D and its BL(1–5) actions will be executed and the result will be as follows:

•  

$\text{POSS}(D)=\text{POSS}(D)\cup \{\{\text{REQUEST},S,D,\text{id},\text{ti},h\mathrm{2}$ , ( $A,B$ ), ( $M_A,M_B)\}$ , $C\mathrm{1}=H(A.B.\mathrm{\hspace{0.17em}\hspace{0.17em}}\{$ REQUEST, $S,D$ , id, ti $\}.K_{SD},\mathrm{\hspace{0.17em}\hspace{0.17em}}\{$ REPLAY, $D,S$ , id, ti, $(A,B)$ , $(M_A,M_B)\})$

 

$\text{BEL}($ D $)=\text{BEL}($ D $)\cup \{\#(\text{ti})\}$

 

$\text{Proof}(D)=\text{Proof}(D)\cup {\{h\mathrm{2}\}}^{*}$

 

Since ${\{h2\}}^{*}$ ∈ Proof(D) we can apply integrity rule RL(18): ${\{h2\}}^{*}\in$ Proof $(D)$ / $\text{BEL}(D)$ = BEL $(D)\cup \{\{\text{REQUEST},S,D,\text{id},\text{ti},h_0,(),()\}$ ∈ Poss(S)}.

After the execution of D(7) and D(8), the POSS set will be updated as follows

•  

POSS(D) = POSS( $D)\cup \{\{$ REQUEST $,S$ , D, id, ti, $h2$ , ( $A,B$ ), $(M_A,M_B)\}$ , C1 = H(A. B. {REQUEST, S, D, id, ti $\}.K_{SD}$ , {REPLAY, $D,S$ , id, ti, $(A,B),(M_A,M_B)\}.K_{DS}$ , $M_D=H(\{$ REPLAY, $D,S$ , id, ti, ( $A,B$ ), $(M_A,M_B)\}.K_{DS})$ .

Therefore, the target (destination) node makes sure that the request is from node S and it will send a reply message using the reverse path since the comparison action confirms equality. Each intermediate node (A and B in our example) will receive the reply, adds its key to the key list, and forwards it to the next node until it reaches the source. The destination will authenticate each intermediate node using the same process as the target node did.

When the target node S receives the REPLY the rest of its actions will be executed to ensure the validity of the target's MAC, and each MAC in the MAC list. Node S local sets will be updated as follows:

•  

POSS $(S)$ = $\{K_{DS},K_{SD},K_{A\text{ti}},K_{B\text{ti}}$ , $(A\bowtie K_{A\text{ti}})$ from A, $(B\bowtie K_{B\text{ti}})$ from B, {REPLY, $D,S$ , ti, $(A,B)$ , $(M_A,M_B)$ , $M_D$ , $(K_{B\text{ti}},K_{A\text{ti}})\}$ , {REPLY, $D,S$ , id, ti, $(A,B)$ , $(M_A,M_B)\}$ . $K_{DS}\}$ , {REQUEST, S, D, id, ti, h1, $(A),()\}.A_{\text{ti}}$ , {REQUEST, $S,D$ , id, ti, $h2$ , $(A,B),()\}.B_{\text{ti}}\}$

 

Proof $(S)=$ Proof $(S)\cup \{\{M_D{\}}^{*}$ , $\{M_B{\}}^{*}$ , $\{M_A{\}}^{*}\}$ .

Now we can apply the authentication rule (RL17) for each entry in the proof set.

Authentication Rule (RL17):

$$\begin{array}{cc}& \frac{(D\bowtie K_{DS})\mathrm{\hspace{0.17em}\hspace{0.17em}}\text{from}\mathrm{\hspace{0.17em}\hspace{0.17em}}D\in \text{POSS}\left(S\right)\mathrm{\hspace{0.17em}\hspace{0.17em}}}{\text{Binding}\left(S\right)=\text{Binding}\left(S\right)\cup \left\{\left(D\bowtie K_{DS}\right)\right\}},\\ \frac{(D\bowtie K_{DS})\in \text{BEL}\left(S\right),{\left\{M_D\right\}}^{*}\in \text{Proof}\left(S\right)}{\text{Binding}\left(S\right)=\text{Binding}\left(S\right)\cup \left\{\left(D\bowtie K_{DS}\right)\right\}},\\ \frac{\left(B\bowtie K_{B\text{ti}}\right)\hspace{0.17em}\hspace{0.17em}\text{from}\mathrm{\hspace{0.17em}\hspace{0.17em}}B\in \text{POSS}\left(S\right)}{\text{Binding}\left(S\right)=\text{Binding}\left(S\right)\cup \left\{\left(B\bowtie K_{B\text{ti}}\right)\right\}},\\ \frac{\left(B\bowtie K_{B\text{ti}}\right)\in \text{BEL}\left(\text{S}\right),{\left\{M_B\right\}}^{*}\in \text{Proof}\left(S\right)}{\text{Binding}\left(S\right)=\text{Binding}\left(S\right)\cup \left\{\left(B\bowtie K_{B\text{ti}}\right)\right\}},\\ \frac{(A\bowtie K_{A\text{ti}})\mathrm{\hspace{0.17em}\hspace{0.17em}}\text{from}\mathrm{\hspace{0.17em}\hspace{0.17em}}A\in \text{POSS}\left(S\right)}{\text{Binding}\left(S\right)=\text{Binding}\left(S\right)\cup \left\{\left(A\bowtie K_{A\text{ti}}\right)\right\}},\\ \frac{(A\bowtie K_{A\text{ti}})\in \text{BEL}\left(S\right),{\left\{M_A\right\}}^{*}\in \text{Proof}\left(S\right)}{\text{Binding}\left(S\right)=\text{Binding}\left(S\right)\cup \left\{\left(A\bowtie K_{A\text{ti}}\right)\right\}}.\end{array}$$

(9)

Also we can apply the integrity rule (RL18) for each entry in the proof set.

Integrity Rule (RL18):

$$\begin{array}{l}{\left\{M_D\right\}}^{*}\\ \hspace{1em}\in \text{Proof}\left(S\right)\times (\text{BEL}\left(S\right):=\text{BEL}\left(S\right)\\ \hspace{1em}\hspace{1em}\cup \{\left\{\text{REPLY},D,S,\text{ti},\left(A,B\right),\left(M_A,M_B\right),M_D,\left(\right)\right\}\\ \hspace{1em}\hspace{1em}{\mathrm{\hspace{0.17em}\hspace{0.17em}}\in \text{Poss}\left(D\right)\})}^{-1}\end{array}$$

(10)

$$\begin{array}{l}{\left\{M_B\right\}}^{*}\\ \hspace{1em}\in \text{Proof}\left(S\right)\times (\text{BEL}\left(S\right):=\text{BEL}\left(S\right)\\ \hspace{1em}\hspace{1em}\cup \{\left\{\text{REPLY},D,S,\text{ti},\left(A,B\right),\left(M_A,M_B\right),M_D,\left(\right)\right\}\\ \hspace{1em}\hspace{1em}{\mathrm{\hspace{0.17em}\hspace{0.17em}}\in \text{Poss}\left(B\right)\})}^{-1}\end{array}$$

(11)

$$\begin{array}{l}{\left\{M_A\right\}}^{*}\\ \hspace{1em}\in \text{Proof}\left(S\right)\times (\text{BEL}\left(S\right):=\text{BEL}\left(S\right)\\ \hspace{1em}\hspace{1em}\cup \{\left\{\text{REPLY},D,S,\text{ti},\left(A,B\right),\left(M_A,M_B\right),{\text{M}}_A,\left(K_{B\text{ti}},K_{A\text{ti}}\right)\right\}\\ \hspace{1em}\hspace{1em}{\mathrm{\hspace{0.17em}\hspace{0.17em}}\in \text{Poss}\left(A\right)\})}^{-1}.\end{array}$$

(12)

Since we applied the authentication and the integrity rules successfully on the target's MAC and on each MAC in the MAC list, it can be concluded that the reply is valid and authenticated; consequently node S can accept it. Therefore, Ariadne achieves both the authentication and the integrity requirements which detect attackers when they attempt to impersonate the message's sender or modify its content.

Flaws in this protocol lie in the assumptions of the authors that may affect the usability of the protocol. Ariadne assumed the presence of a working public key infrastructure (PKI) or certificate authority (CA). Consequently, key management services are assumed to be already existed but are not provided by Ariadne. Also, Ariadne did not take the possibility of having internal attackers into consideration and therefore, no IDS are applied to detect them.

Based on the above assumptions, actions such as ACT₆, ACT₁₁, ACT₁₃, ACT₁₄, ACT₁₆, ACT₁₉, ACT₂₂, ACT₂₄, ACT₂₅, ACT₂₆, ACT₂₇, and ACT₂₈ cannot be activated and rules like R4, R5, R9, R10, and R11 cannot be applied. Based on this observation, LBSA can detect the absence of key management system and IDS in Ariadne. As a result, key management services will fail and intruders cannot be detected.

8. Conclusions and Future Work

The success of applications over multihop communication networks principally depends on the achievement of security requirements. Many secure protocols are proposed, consequently, there should be a reliable way to test if these protocols satisfy the security requirements as their designers claim.

Previous attempts to utilize logic in analyzing security have either focused on a specific requirement or a specific protocol. In this paper, we proposed a logic-based security architecture (LBSA) to specify and analyze any security requirement in any system providing multihop communication using logic. Any system or protocol claiming security can be mapped into our architecture in other words it must be specified using various global/local sets and actions, then it can be analyzed by applying different rules. LBSA provides a formal way to analyze security enforcers and security protocols instead of depending only on the simulation tools which are arguable by many researchers in terms of implementation accuracy.

Additionally, using simulation tools usually covers a small set of scenarios whereas using LBSA more cases can be covered that usually cannot be covered exhaustively by simulation tools.

This paper also illustrated how LBSA can be used to verify security enforcers by applying it to two well-known enforcers which are MAC and digital certificate. In addition to that, a case study for a secure routing protocol used in ad hoc and sensor networks named Ariadne was also evaluated in terms of security using LBSA.

To the best of our knowledge, the proposed security architecture covers the most important enforcers. Further development of new enforcers in the future may simply need other sets, actions, and rules to be added. Also, LBSA could be extended by considering new rules and actions for the Interaction between Intrusion Detection System (IDS) and Intrusion Prevention System (IPS). Moreover, LBSA can utilize the computational Intelligence tools in analyzing the security.