Neuman Stubblebine

Purpose

It involves bringing about the exchange of some ticket and the second is a protocol for multiple authentications.

Informal Specification

  1. A -> B : A,Na
  2. B -> S : B,E(Kbs : A, Na, tb), Nb
  3. S -> A : E(Kas : B, Kab, Na, tb), E(Kbs : A, Kab, tb), Nb
  4. A -> B : E(Kbs : A, Kab, tb), E(Kab : Nb)
  5. A -> B : N'a, E(Kbs : A, Kab, tb)
  6. B -> A : N'B, E(Kab : N'a)
  7. A -> B : E(Kab : N'b)

See Commonly Used Representations
  tb - timestamp

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 17 August 2007
--- Neuman Stubblebine
---     A -> B : A,Na
---     B -> S : B,E(Kbs : A, Na, tb), Nb
---     S -> A : E(Kas : B, Kab, Na, tb), E(Kbs : A, Kab, tb), Nb
---     A -> B : E(Kbs : A, Kab, tb), E(Kab : Nb)
---     A -> B : N'a, E(Kbs : A, Kab, tb)
---     B -> A : N'B, E(Kab : N'a)
---     A -> B : E(Kab : N'b)

(reset)
(
module neuman
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.
time : type.                            time <: msg.

enc : key -> msg -> msg.

net : msg -> state.

GL : time -> {A : princ} {B : princ} stk A B -> state.

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

YRule4:
   forall Kab : stk A B.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Na : nonce.
   forall Nb : nonce.
    net(enc Kas (B & Kab & Na & Tb) & enc Kbs (A & Kab & Tb) & Nb), L Na
   => net(enc Kbs (A & Kab & Tb) & enc Kab Nb).
}


receiver:
forall B : princ.
{
			exists L: nonce -> nonce -> {B : princ} {S : server} ltk B S -> state.
YRule2:
  forall A : princ.
  forall S : server.
  forall Kbs : ltk B S.
  forall Na : nonce.
    net(A & Na)
 => exists Nb : nonce.
   net(B & enc Kbs (A & Na & Tb) & Nb), L Na Nb B S Kbs.

YRule5:
   forall A : princ.
   forall S : server.
   forall Kab : stk A B.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Na : nonce.
   forall Nb : nonce.
   forall Tb : time.
    net(enc Kbs (A & Kab & Tb) & enc Kab Nb), L Na Nb B S Kbs
   => GL Tb A B Kab.

}


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


initiator2:
forall A : princ.
{
			exists L: nonce -> {A : princ} {B : princ} stk A B -> state.
YRule5:
  forall B : princ.
  forall Tb : time.
  forall Kab : stk A B.
  forall Kbs : ltk B S.
  GL Tb A B Kab
  => exists N'a : nonce.
   net(N'a & enc Kbs (A & Kab & Tb)), L N'a A B Kab.

YRule7: 
  forall B : princ. 
  forall Kab : stk A B.
  forall N'a : nonce.
   net(N'b & enc Kab (N'a)), L N'a A B Kab
  => net(enc Kab (N'b)).

}


receiver2:
forall B : princ.
{
			exists L: nonce -> {A : princ} {B : princ} stk A B -> state.
YRule6:
  forall A : princ.
  forall Kab : stk A B.
  forall Kbs : ltk B S.
  forall N'a : nonce.
  forall Tb : time. 
   net(N'a & enc Kbs (A & Kab & Tb))
 => exists N'b : nonce.
   net(N'b & enc Kab (N'a)), L N'b A B Kab.

YRule8:
   forall N'b : nonce. 
   forall Kab : stk A B.
   forall N'b : nonce.
   forall Tb : time.
    net(enc Kab (N'b)), L N'b A B Kab
   => empty.

}

)
 

Findings

Another example of repeatation, although on a smaller scale than kerberos.