PROTOCOL:
IEEE802.1x - EAPOL: EAP over LAN authentication
(IEEE 802.1X RADIUS: Remote Authentication Dial In User Service)

 

PURPOSE:

The 802.1X (EAPOL) protocol provides effective authentication regardless of whether one implements 802.11 WEP keys or no encryption at all. If configured to implement dynamic key exchange, the 802.1X authentication server can return session keys to the access point along with the accept message. The access point uses the session keys to build, sign and encrypt an EAP key message that is sent to the client immediately after sending the success message. The client can then use contents of the key message to define applicable encryption keys.

 

REFERENCE:

 

MODELER:

 

ALICE_BOB:

 Client -> Authenticator : EAPOL_Start
 Auth -> Client : EAPOL_Request_Identity
 Client -> Auth : EAPOL_Response (= NAS_ID, NAS_PORT, {Secret_Key}MD5)
 Auth -> Server : Access-Request (= NAS_ID, NAS_PORT, {Secret_Key}MD5)
 Server -> Auth : Access-Challenge 
 Auth -> Client : Access-Challenge 
           where  Access-Challenge = Message    
 Client -> Auth : Access-Chall-Response 
           where  Access-Chall-Response : {Message}Secret_Key
 Auth -> Server : Access-Chall_Response 
 Server -> Auth : Access_Accept
 Auth -> Client : EAPOL_Success

 

PROBLEMS:
2
 

ATTACKS:
None

 

NOTES:

Agents involved: Client, Authenticator, Radius Server

 



HLPSL:

role client(C,A,S              : agent,
            Kcs                : symmetric_key,
            Md5                : hash_func,
            EAPOL_Success,
            EAPOL_Start,
            EAPOL_Req_Identity : text,
            Success            : text,
            SND, RCV           : channel(dy))
played_by C def=

            local  State             : nat,
                   NAS_ID , NAS_Port : text,
                   Chall_Message     : text

            const  kcs       : protocol_id,
                   sec_c_Kcs : protocol_id
                   
            init State := 0
            
            transition

            1. State  = 0 /\ RCV(start) =|>
               State':= 1 /\ SND(EAPOL_Start)
               
            2. State  = 1 /\ RCV(EAPOL_Req_Identity) =|>
               State':= 2 /\ NAS_ID':=new() /\ NAS_Port':=new()
                          /\ SND(NAS_ID'.NAS_Port'.Md5(Kcs))
                          /\ secret(Kcs,sec_c_Kcs,{C,S})         
                         
            3. State  = 2 /\ RCV(NAS_ID.Chall_Message') =|>
               State':= 3 /\ SND(NAS_ID.{Chall_Message'}_Kcs)
                          /\ witness(C,S,kcs,Kcs)

            4. State  = 3 /\ RCV(NAS_ID.EAPOL_Success) =|>
               State':= 4 /\ SND(NAS_ID.Success)
end role

role auth( C,A,S : agent, Kcs : symmetric_key, Md5 : hash_func, EAPOL_Success, EAPOL_Start, EAPOL_Req_Identity : text, Success : text, Access_accept : text, SND, RCV : channel(dy)) played_by A def= local State : nat, NAS_ID , NAS_Port : text, Chall_message : text, Client_chall_reply : {text}_symmetric_key const kcs : protocol_id init State := 11 transition 1. State = 11 /\ RCV(EAPOL_Start) =|> State':= 12 /\ SND(EAPOL_Req_Identity) 2. State = 12 /\ RCV(NAS_ID'.NAS_Port'.Md5(Kcs)) =|> State':= 13 /\ SND(NAS_ID'.NAS_Port'.Md5(Kcs)) 3. State = 13 /\ RCV(NAS_ID.Chall_message') =|> State':= 14 /\ SND(NAS_ID.Chall_message') 4. State = 14 /\ RCV(NAS_ID.Client_chall_reply') =|> State':= 15 /\ SND(NAS_ID.Client_chall_reply') 5. State = 15 /\ RCV(NAS_ID.Access_accept) =|> State':= 16 /\ SND(EAPOL_Success) 6. State = 16 /\ RCV(NAS_ID.Success) =|> State':= 17 end role
role server(C,A,S : agent, Kcs : symmetric_key, Md5 : hash_func, Success, Failure : text, Access_accept,Access_reject : text, SND, RCV : channel(dy)) played_by S def= local State : nat, NAS_ID , NAS_Port : text, Chall_Message : text const kcs : protocol_id, sec_s_Kcs : protocol_id init State := 21 transition s5. State = 21 /\ RCV(NAS_ID'.NAS_Port'.Md5(Kcs)) =|> State':= 26 /\ Chall_Message':=new() /\ SND(NAS_ID'.Chall_Message') /\ secret(Kcs,sec_s_Kcs,{C,S}) s6. State = 26 /\ RCV(NAS_ID.{Chall_Message}_Kcs) =|> State':= 27 /\ SND(NAS_ID.Access_accept) /\ request(S,C,kcs,Kcs) s7. State = 27 /\ RCV(NAS_ID.Success) =|> State':= 28 end role
role session(C,A,S : agent, Kcs : symmetric_key, Md5 : hash_func, Success, Failure : text, Access_accept, Access_reject : text, EAPOL_Success, EAPOL_Start, EAPOL_Req_Identity : text) def= local S1, S2, S3 : channel (dy), R1, R2, R3 : channel (dy) composition client(C,A,S,Kcs,Md5, EAPOL_Success,EAPOL_Start,EAPOL_Req_Identity, Success,S1,R1) /\ auth(C,A,S,Kcs,Md5, EAPOL_Success,EAPOL_Start,EAPOL_Req_Identity, Success,Access_accept,S2,R2) /\ server(C,A,S,Kcs,Md5, Success,Failure,Access_accept,Access_reject, S3,R3) end role
role environment() def= const c1,a1,s1 : agent, kcsk , kisk, kcik : symmetric_key, md5 : hash_func, succs, fails : text, acc_acp, acc_rej : text, eap_succ, eap_start, eap_req_id : text intruder_knowledge = {c1,a1,s1, md5, kisk,kcik, succs, fails, acc_acp, acc_rej, eap_succ, eap_start, eap_req_id } composition session(c1,a1,s1,kcsk,md5,succs,fails,acc_acp,acc_rej, eap_succ, eap_start,eap_req_id) %/\ session(i,a1,s1,kisk,md5,succs,fails,acc_acp,acc_rej, % eap_succ, eap_start,eap_req_id) end role
goal %secrecy_of Kcs secrecy_of sec_c_Kcs, sec_s_Kcs %Server authenticates Client on kcs authentication_on kcs end goal
environment()