Gong Mutual Authentication Protocol

Purpose

It is a mutual authentication protocol of two principals with a trusted server, and exchange of a new symmetric key. Uses one-way functions and no encryption.
f and g are one way publicly known functions. the principal A and B shares a secret Pa and Pb respectively, with the authentication server. xor is the xor function and equals is the equality function. Ha and Hb are handshake numbers
In message 3 (k,ha,hb) = f(Ns, Na, B, Pa) is calculated by the server. K is the secret to be shared between A and B. B computes f(Ns, Nb, A , Pb) to retrieve (K,Ha,Hb) from the second item of the message. It also computes g(K,Ha,Hb,Pb) to check against the third item that tampering has not taken place. A computes f(Ns,Na,B,Pa) to get (K,Ha,Hb). If the value of Hb matches the one sent by B then A replies with message 5.

Informal Specification

  1. A -> B : A,B,Na
  2. B -> S : A, B, Na, Nb
  3. S -> B : Ns, f(Ns,Nb,A,Pb) xor (K,Ha,Hb), g(K,Ha,Hb,Pb)
  4. B -> A : Ns,Hb
  5. A -> B : Ha

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 28 October 2007
--- Gong Mutual Authentication Protocol
---     A -> B : A,B,Na
---     B -> S : A, B, Na, Nb
---     S -> B : Ns, f(Ns,Nb,A,Pb) xor (K,Ha,Hb), g(K,Ha,Hb,Pb)
---     B -> A : Ns,Hb
---     A -> B : Ha

(reset)
(
module GMAP
export * .

server : type.                         server <: princ.
key : type.                            key <: msg.
nonce : type.                           nonce <: msg.
time : type.                           time <: msg.
xor : msg -> msg -> msg.
f : msg -> msg -> msg -> msg -> msg.
g : msg -> msg -> msg -> msg -> msg.
m : msg -> msg -> msg -> msg.
equal : msg -> msg -> msg.
net : msg -> state.
initiator:
forall A : princ.
{
                exists LA : nonce -> state.
GRule1:
  empty
  => exists Na : nonce.
   net(A & B & Na), LA Na.

GRule5:
  forall Na : nonce.
  forall Ns : nonce.
  forall Pa : msg.
  forall Hb : msg.
  forall Ha : msg.
  forall k : key.
    net(Ns & Hb)
   => net(Ha) , LA Na
   if (equal (f Ns Na B Pa)(k & Ha & Hb)).
}


receiver:
forall B : princ.
{
                  exists LB1 : nonce -> nonce -> state.
                  exists LB2 : msg -> state.
GRule2:
  forall A : princ.
  forall Na : nonce.
    net(A & B & Na)
 => exists Nb : nonce.
   net(Nb & A & Na & B), LB1 Na Nb.

GRule4:
   forall A : princ.
   forall Hb : msg.
   forall Ha : msg.
   forall Pb : msg.
   forall M : msg.
   forall N : msg.
   forall Ns : nonce.
   forall Na : nonce.
   forall Nb : nonce.
   forall k : key.
     net(Ns & M & N), LB1 Na Nb
  => net(Ns & Hb), LB2 Ha
  if (xor M (equal (f Ns Nb A Pb) ( k & Ha & Hb))) & (equal N (g K Ha Hb Pb)).

GRule6:
   forall Ha : msg.
   net(Ha), LB2 Ha
   => empty.

}


server:
forall S : server.
{
GRule3:
   forall A : princ.
   forall B : princ.
   forall Hb : msg.
   forall Ha : msg.
   forall Pb : msg.
   forall Na : nonce.
   forall Nb : nonce.
   forall k : key.
    net(Nb & A & Na & B)
     => exists Ns : nonce.
        net(Ns & xor (f Ns Nb A Pb) T & (g k Ha Hb Pb))
     if equal (f Ns Na B Pa) T & equal T (k & Ha & Hb).
}


)
 

Findings