1. Introduction

Wireless users are increasing day by day. This calls for need of secure communication between wireless Stations (STA) and Access Point (AP). WEP (Wired Equivalent Privacy), WPA (Wi-Fi Protected Access) and WPA-2 (IEEE 802.11i[1][2]) are three standard ways for controlling the network access and evolving the secret shared key in Wireless Local Area Networks (WLANs). Out of these WEP is currently deprecated due to inherent weaknesses[3-6]. WPA was an interim security standard, requiring software up-gradation of nodes. In year 2004, WPA-2 (IEEE 802.11i[1]) came into existence and is continuing till date. The standard is stable and provides security to data frames. Still the standard has scope for improvisations.

Research community and societies are working to make WLANs robust and secure. In this regard, Secure WLAN Authentication Scheme (SWAS), a delegation based[7-8] scheme is proposed at[9] to provide access and shared key generation between STAs and AP. It involves cryptographic operations for providing a secure key exchange. It evolves fresh keys for securing data sessions. The scheme not only provide entity authentication but also provide authentication to the individual frames involved. It also reduces the entire process of authentication and key generation to only four messages. In 802.11i authentication, with Extensible Authentication Protocol-Transport Layer Security (EAP-TLS) as EAP method, several messages are exchanged between STA & AP and between AP & AS. After this, 4-way handshake is done to evolve fresh keys between STA and AP. Thus, SWAS scheme reduces communication and network overload. The average computation time for SWAS authentication is of the order of 21.8477 ms while on the same set of systems authentication time for 802.11i with EAP-TLS is of the order of 76.8 ms. Thus, the extra computations used in the SWAS does not have much effect.

For enhancing the protocol’s security, its properties need to be validated. In this paper, we present a formal proof of the secrecy property of SWAS using extended Protocol Composition Logic (PCL) which is a formal method used for validating the security properties of a protocol.

The rest of the paper is divided into 4 sections. Section 2 presents a brief review of Secure WLAN Authentication Scheme (SWAS). Section 3 discuss the methodology and axioms used. Section 4 provides formal proof of secrecy property of SWAS. Section 5 provides conclusions. Appendix A shows fragment of proof system while Appendix B provides statements of formal proof of secrecy property

2. Review of Secure WLAN Authentication Scheme (SWAS)

We proposed Secure WLAN Authentication Scheme (SWAS) at[9]. It is used for providing entity authentication, access control and fresh key generation. During the authentication process, security of keys and frame contents is maintained. All messages in the scheme either use symmetric key encryption or Message Integrity Code (MIC) for protecting the contents. For this purpose, the scheme has several keys (Master Key (MK), Master Session Key (MSK), Pairwise Master Key (PMK) and Pairwise Transient Key (PTK) mapped to equivalent key hierarchy of 802.11i. The end of SWAS authentication process leads to evolving of a secure key (PTK) for protecting the data frames transmitted between STA and AP.

SWAS is a delegation based[7-8] scheme and has initialization phase, request phase and authentication phase. The initialization phase is used to register the STA with the authentication server (AS). Once registered, the STA is given delegation key (σ), securely. The elliptic curve parameters and public keys (PK_AP-PK_STA) are shared in the request phase. These are used for evolving the master key (MK) using elliptic curve diffie-hellman (ECDH) key generation algorithm. In the authentication phase, STA uses the delegation key for generating the delegation passcode (and ) which is embedded in message M1. STA also keeps the AS passcode in the M1. The messages used in the scheme are listed and described in table 1 (For simplicity, some of the contents are removed). The purpose and contents of passcodes in the scheme are mentioned in table 2. Delegation passcode is verified at the AP. Its verification authenticates the STA. AP forwards the AS passcode to the AS in M2. It also signs the message M2 digitally. AS authenticates AP via digital signature then decrypts the AS passcode, extracts the random number r3. AS creates the digitally signed message M3 and sends it back to AP. M3 contains the AP passcode and STA passcode. From AP passocode, AP extracts r3 and derives the pairwise master key (PMK) and pairwise transient key (PTK). Using STA passcode, the STA is ensured that the genuine AS is involved in the authentication process. Thus all devices confirm each other’s identity.

The AS passcode, AP passcode and STA passcode are all encrypted using keys known only to the sender and receiver. The messages M1 & M4 are protected using MIC while M2 & M3 are digitally signed. The secrecy property imply that the secret keys derived using the material (random numbers r1, r2, r3 and serial number s1) in M1, M2, M3 and M4 remains secret and shared between the desired parties. The keys used in the SWAS scheme are described in table 3. The MK (master key), MSK (master session key), PMK (pairwise master key) and PTK (pairwise transient key) are shared between STA and AP. No other party can calculate these keys. The PTK is used to encrypt the data frames between STA and AP.

SWAS enhances network performance. It utilizes only 4 messages for authentication and key exchange. Two (2) messages are utilized between STA and AP while two (2) are utilized between AP and AS. Whereas, IEEE 802.11i (the standard WLAN security protocol) utilizes large number of messages for the same purpose. A total of nine (9) messages are exchanged between STA and AP while eight (8) messages are exchanged between AP and AS during default EAP-TLS authentication. Four (4) messages are also exchanged between STA and AP during four way handshake that follows EAP-TLS authentication.

Table 1. SWAS Message description

Table 2. SWAS Passcodes

Table 3. SWAS Keys Key Shared between Calculated as MK STA and AP Calculated using ECDH MSK STA and AP PRF{ r1, MK } KAP-AS STA, AP, and AS PRF{ r2, MK } PMK STA and AP PRF{ r3, MSK } PTK STA and AP PRF{s1, PMK }

3. Methodology and Axioms Used

The Protocol Composition Logic (PCL)[10-13] is used extensively for proving the security properties like authentication property of a protocol. For proving the secrecy property, in this paper extended PCL[14] by Roy et al. (2008) is used. This extended version of PCL has additional formulas, rules and axioms (in addition to that of PCL). The secrecy properties are formalized using the Has(, s) predicate. It expresses the fact that principal , has the information needed to compute the secret s. SendsSafeMsg(X, s, ) formulates the safe sending of all messages by thread X. SafeNet (s, ) is used for safe sending by all threads. Predicate SafeNet (M, s, ) asserts that every occurrence of s in message M is protected by a key in the set . The NET rule deals with the safety of all messages in the network assuming all messages in the network were safe prior to that step; provided “each possible protocol step” locally sends out safe messages.

We mention the fragment of PCL proof system considered for proof in Appendix A. It shows only the axioms used in proving the SWAS properties. A comprehensive list of axioms is present in appendix A at[10] and[14]. The Honesty Rule is considered which states that an honest principal is suppose to follow one or more roles of the protocol i.e. it must satisfy every invariant property of the protocol role.

4. Proof of Secrecy Property of SWAS

Secrecy property asserts that some data (keys and other secret information) that are used in the protocol are not revealed to others. In case of encrypted messages, only the agents that have the decryption key can obtain the information. The extended logic involves general approach for the cases where protocol agent receives data encrypted by one of the chosen set of encryption keys, only sends sensitive data under encryption by another key in the set. This approach reduces complexity in proving the secrecy of protocol.

The secrecy properties of SWAS w.r.t. extended PCL logic are listed in table 4. The secrecy objective is expressed in a form that the secret information is known only to certain principals. For ex. means that when the thread C finishes executing the client’s (STAs) role, the key MSK remains secret. Similarly, other security properties are analogously defined. Hence, we intend to prove:

For proving these properties certain conditions Φ are assumed (Appendix A), along with the honesty of the principals . It is then proved (Appendix B) using secrecy induction that this implies SafeNet(MSK,),

Table 4. SWAS secrecy properties

SafeNet(K_AP-AS,) and SafeNet(PTK,). POS axiom is then utilized to conclude the SWAS secrecy proof. We are not showing the SWAS secrecy property w.r.t. PMK due to similarity and space constraint.

5. Conclusions

A Secure WLAN Authentication Scheme (SWAS) is an effort towards building a secure authentication with desired security properties. The scheme asserts to improve the security in WLANs as all its packets are protected using cryptographic measures. It maintains message protection while keeping low network overhead and hence, increases network performance. Strengthening the security of the scheme implies enhancing reliability of the WLAN communication system (key and data exchange). Secrecy is one of its major property through which the scheme strengthen the security. In this paper, we proof the secrecy property of the SWAS using extended protocol composition logic method. As future work we intend to prove the other properties like authentication and resistance to DoS (Denial of Service) attacks.

Appendix A

Fragment of the PCL Proof System

Axioms and Rules for proving SWAS secrecy property

SendsSafemsg (X,s,) ≡ ∀M. (Send (X,M) ⊃ SafeMsg(M,s,K)

SafeNet (s,) ≡ ∀X. SendsSafeMsg(X,s,)

SAF0SafeMsg(s,s,) ⊥ SafeMsg(x,s,), Where x is an atomic term different from s

SAF1SafeMsg(M₀,M₁,s,) ≡ SafeMsg (M_0,s,) SafeMsg(M₁,s,)

SAF2SafeMsg(E_sym[k] (M),s,) ≡ SafeMsg (M_,s,) k ∈

SAF4SafeMsg(HASH (M), s,)

NET

(*): does not capture free variables in , , s, and is prefix closed.

NET0SafeNet(s,)[]_x SendsSafeMsg(X,s,)

NET1SafeNet(s,)[receive M]_x SafeMsg(M,s,)

NET2SendsSafeMsg(X,s,)[a]_x SendsSafeMsg(X,s,),where a is not a send.

NET3SendsSafeMsg(X,s,)[send M]_x SafeMsg(M,s,) ⊃SendsSafeMsg(X,s,)

POSSafeNet(s,) Has(X,M) SafeMsg(M,s,)⊃ ∃ k∈, Has(X,k) New(X,s)

Environmental Assumptions:

Secrecy is proved w.r.t. key set = (K_AP-AS, σ, MK, MSK, PMK, PTK)

Where, r1 ≠ r2 ≠ r3 ≠ s1 ≠ K_AP-AS ≠ MSK ≠ PTK ≠ MK ≠σ

i.e. all keys in the scheme belongs to set and none of them is equal to each other and to the chosen random numbers.

The assumed condition Φ is conjunction of following formulas:

Φ₁: ∀X, M, New(X,k) ⊃ (Send(X,M) ContainsOpen (M,k))

Where, ContainsOpen is used to assert that k can be obtained without any decryption.

Φ₂: ∀X, . New (X,K_AP-AS) SymEnc(X,r3.K_AP-AS, σ)

New Formulas:

1. Assign(X, x, y): x is assigned value y by thread X

2. Derieve(X, k, x, y): thread X calculates key k from x and y using pseudo random function (PRF)

Derieve(X, k, x, y) ≡ Assign(X,k,Computes(X,PRF{x, y}))

For ex. Derieve(X, MSK, x, y) ≡ Assign(X, MSK, Computes(X,PRF{r1,MK}))

New Axioms:

SAF5: SafeMsg(HASH_k(M) ,s,) ≡ SafeMsg(MIC_k,s,) where MIC_k is MIC of M using k, k∈

DER : New(X,k_new) ≡ New(X,x) Derieve(X, k_new, x, y)

Derivation of key using new random number x leads to new key (k_new) formation.

NET4: SafeNet(M,s,)[ derieve k_new, x, s)]_XSendsSafeMsg(, s,)

It is safe to send a MIC of the message obtained using the new derieved key

Appendix B

Proof of secrecy property, SWAS:

Let[STA] : [new r1, r2, r3, s1;

derive MSK, r1, MK;

derive K_AP-AS , r2, MK;

enc_CA: =symenc s1.r2,MK;

tc := symenc r3. K_AP-AS, σ;

MIC_MSK = HASH _MSK(Msg1);

send enc_CA.tc. MIC_MSK ;]

case (i) w.r.t. MSK

(1)

(2)

DER, (2) [STA] New(, K_AP-AS) Send(, IDAS. E_sym[MK] (s1.r2).

(3)

(4)

NET4, (1), (4) [STA] SafeMsg(IDAS. E_sym[MK] (s1.r2). E_sym[σ] (r3.

(5)

(6)

case (ii) w.r.t. K_AP-AS

(7)

(8)

(9)

(10)

(11)

Let[AP] : [receive IDAS.enc_CA.tc. MIC_MSK ;

text_CA: =symdec enc_CA, MK;

match text_CA as s1.r2;

derieve K_AP-AS, r2, MK;

(Msg2);

send tc. . DigSig_AP;]

case (i) w.r.t. MSK

(12)

(13)

(14)

case (ii) w.r.t. KAP-AS

(15)

(16)

(17)

(18)

Let[AS] : [receive tc. . DigSig_AP ;

text_tc: = symdec tc, σ;

match text_tc as r3. K_AP-AS;

enc_SA: = symenc IDSTA.r3, K_AP-AS;

ts: = symenc IDAP.r3, σ;

send enc_SA.ts.DigSig_AS;]

NET1, SAF1 SafeNet (K_AP-AS, )[ receive tc. .DigSig_AP] SafeMsg

(19)

SAF*,(19) SafeNet (K_AP-AS, )[ receive tc. .DigSig_AP] SafeMsg

(20)

SAF2,(20) SafeNet (K_AP-AS, )[ receive tc. .DigSig_AP] SafeMsg

(21)

SAF2,(20) SafeNet (K_AP-AS, )[ receive tc. .DigSig_AP]

(22)

SAF1,(21),(22) SafeNet (K_AP-AS, )[ receive tc. .DigSig_AP]

(23)

(24)

Precondition : Receive(, E_sym[MK](s1,r2))

Let[AP] : [receive enc_SA.ts.DigSig_AS ;

text_SA: = symdec enc_SA, K_AP-AS;

match text_SA as IDSTA.r3;

enc_AC : =symenc s1.r3, PTK;

send enc_AC.ts;]

case (i) w.r.t. KAP-AS

(25)

(26)

(27)

(28)

(29)

(30)

case (ii) w.r.t. PTK

(31)

(32)

(33)

(34)

(35)

(36)

(37)

(38)

(39)

(40)