EAP-Archie is a native EAP authentication method [20]. Therefore, there is no defined stand-alone version of Archie outside EAP. Archie is one of the symmetric cryptography methods that use a pre-shared secret key. The Archie� 512-bit shared secret key consists of two 128-bit keys called key-confirmation key (KCK), key-encryption key (KEK), and the 256-bit key-derivation key (KDK). The key-confirmation key is used for mutual authentication. The key-encryption key is used for distributing the secret nonces for session key derivation. The key-derivation key is used for deriving the session keys.
Note: the original draft has expired. The new version is EAP-PSK.
S -> P: request_id
P -> S: respond_id.P
S -> P: S.SessionID
P -> S: SessionID.P.{nonceP}_KEK.Bind.MAC1
S -> P: SessionID.{nonceA}_KEK.Bind.MAC2
P -> S: SessionID.MAC3
- SessionID: Nonce
- KCK: Shared Key used for Authentication
- KEK: Shared Key used for Encryption
- KDK: Shared Key used for Key Derivation
- EMK: EAP Master Key: PRF(KDK.nonceA.nonceP)
- MAC1: MAC(KCK.S.SessionID.P.{nonceP}_KEK.Bind)
- MAC2: MAC(KCK.P.{nonceP}_KEK.SessionID.{nonceA}_KEK.Bind)
- MAC3: MAC(KCK.SessionID)
- Bind: addressing information (address_of_peer,address_of_server)
role peer (
P,S : agent,
MAC : hash_func,
KEK,KCK,KDK : symmetric_key,
SND,RCV : channel (dy))
played_by P def=
local
Np,Bind : text,
Na,Sd : text, % Sd (=SessionID)
State : nat
const
request_id,
respond_id : text,
sec_np,
na,np,sd,bind : protocol_id
init
State := 0
transition
0. State = 0 /\ RCV(request_id) =|>
State' := 1 /\ SND(respond_id.P)
1. State = 1 /\ RCV(S.Sd') =|>
State' := 2 /\ Np' := new()
/\ Bind' := new()
/\ SND(Sd'.P.
{Np'}_KEK.Bind'.
MAC(KCK.S.Sd'.P.{Np'}_KEK.Bind'))
/\ secret(Np',sec_np,{P,S})
/\ witness(P,S,np,Np')
/\ witness(P,S,bind,Bind')
2. State = 2 /\ RCV(Sd.{Na'}_KEK.Bind.
MAC(KCK.P.{Np}_KEK.Sd.{Na'}_KEK.Bind)) =|>
State' := 4 /\ SND(Sd.MAC(KCK.Sd))
/\ request(P,S,sd,Sd)
/\ request(P,S,na,Na')
end role
role server (
S,P : agent,
MAC : hash_func,
KEK,KCK,KDK : symmetric_key,
SND,RCV : channel (dy))
played_by S def=
local
Np,Bind : text,
Na,Sd : text,
State : nat
const
request_id,
respond_id : text,
sec_na,
na,np,sd,bind : protocol_id
init
State := 0
transition
0. State = 0 /\ RCV(start) =|>
State' := 1 /\ SND(request_id)
1. State = 1 /\ RCV(respond_id.P) =|>
State' := 3 /\ Sd' := new()
/\ SND(S.Sd')
/\ witness(S,P,sd,Sd')
2. State = 3 /\ RCV(Sd.P.{Np'}_KEK.Bind'.
MAC(KCK.S.Sd.P.{Np'}_KEK.Bind')) =|>
State' := 5 /\ Na' := new()
/\ SND(Sd.{Na'}_KEK.Bind'.
MAC(KCK.P.{Np'}_KEK.Sd.{Na'}_KEK.Bind'))
/\ witness(S,P,na,Na')
/\ request(S,P,np,Np')
/\ request(S,P,bind,Bind')
/\ secret(Na',sec_na,{P,S})
3. State = 5 /\ RCV(Sd.MAC(KCK.Sd)) =|>
State' := 7
end role
role session (
S,P : agent,
MAC,PRF : hash_func,
KEK,KCK,KDK : symmetric_key)
def=
local Speer,Rpeer,Sserver,Rserver : channel (dy)
composition
peer( P,S,MAC,KEK,KCK,KDK,Speer,Rpeer)
/\ server(S,P,MAC,KEK,KCK,KDK,Sserver,Rserver)
end role
role environment()
def=
const
s,p : agent,
mac,prf : hash_func,
kek,kck,kdk : symmetric_key,
kek_is,kck_is,kdk_is : symmetric_key,
kek_ip,kck_ip,kdk_ip : symmetric_key,
sd,na,np,bind : protocol_id
intruder_knowledge = {s,p,mac,prf}
composition
session(s,p,mac,prf,kek,kck,kdk)
/\ session(s,p,mac,prf,kek,kck,kdk)
end role
% - P wants to be sure that S sent SessionID and nonceA.
% - S wants to be sure that P sent nonceP and Bind.
% - Secrecy of nonceA and nonceP, which are used for key derivation.
goal
%Peer authenticates Server on sd
authentication_on sd
%Peer authenticates Server on na
authentication_on na
%Server authenticates Peer on bind
authentication_on bind
%Server authenticates Peer on np
authentication_on np
%secrecy_of Na, Np
secrecy_of sec_na, sec_np
end goal
environment()