Kao Chow Repeated Authentication Protocol

Purpose

It is not susceptible to the attacks on the Neuman Stubblebine

Informal Specification

  1. A -> S : A,B,Na
  2. S -> B : E(Kas: Na,Kab,A,B),E(Kbs: Na,Kab,A,B)
  3. B -> A : E(Kas: Na,Kab,A,B),E(Kab: Na), Nb
  4. A -> B : E(Kab: Nb)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 10 September 2007
--- Kao Chow Repeated Authentication Protocol
---     A -> S : A,B,Na
---     S -> B : E(Kas: Na,Kab,A,B),E(Kbs: Na,Kab,A,B)
---     B -> A : E(Kas: Na,Kab,A,B),E(Kab: Na), Nb
---     A -> B : E(Kab: Nb)
(reset)
(
module KaoChow
export * .

server : type.                         server <: princ.
key : type.
stk : princ -> princ -> type.          stk A B <: msg.  stk A B <: key.
ltk : princ -> princ -> type.          ltk A B <: key.
nonce : type.                           nonce  <: msg.

enc : key -> msg -> msg.

net : msg -> state.

initiator:
forall A : princ.
{
                          exists LA : nonce -> princ -> state.
KCule1:
  forall B : princ.
  empty => 
   exists Na : nonce.
  net(A & B & Na), LA Na B.

KCRule4: 
   forall B : princ.
   forall Kab : stk A B.
   forall Kbs : ltk B S.
   forall Kas : ltk A S.
   forall Na : nonce.
   forall Na : nonce.
    net(enc Kas (A & B & Na & Kab) & enc Kab Na & Nb), LA Na B
  => net(enc Kab Nb).

}


receiver:
forall B : princ.
{
                          exists LB : nonce -> {A : princ} {B : princ} stk A B -> state.
KCRule3: 
   forall A : princ.
   forall Kab : stk A B.
   forall Kbs : ltk B S.
   forall Kas : ltk A S.
   forall Na : nonce.
    net(enc Kas (A & B & Na & Kab) & enc Kbs (A & B & Na & Kab))
 => exists Nb : nonce.
    net(enc Kas (A & B & Na & Kab) & enc Kab Na & Nb), LB Nb A B Kab.

KCRule5:
   forall A : princ.
   forall Kab : stk A B.
   forall Nb : nonce.
   net(enc Kab Nb), LB Nb A B Kab
 => empty.

}


server:
forall S : server.
{
KCRule2:
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Na : nonce.
  net(A & B & Na)
 => exists Kab : stk A B.
    net(enc Kas (A & B & Na & Kab) & enc Kbs (A & B & Na & Kab)).

}

)