Otway-Rees Protocol

Purpose

The nonce M identifies the session number.Kas and Kbs are symmetric keys whose values are initially known only by A and S, respectively B and S. Kab is a fresh symmetric key generated by S in message 3 and distributed to B, directly in message 3, and to A, indirectly, when B forwards blindly {Na, Kab}Kas to A in message 4.

Informal Specification

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

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 13 June 2007
--- Otway-Rees Protocol
---     A -> B : M,A,B,E(Kas: Na,M,A,B)
---     B -> S : M,A,B,E(Kas: Na,M,A,B),E(Kbs: Nb,M,A,B)
---     S -> B : M,E(Kas: Kab,Na),E(Kbs: Kab,Nb)
---     B -> A : M,E(Kas: Kab,Na)
(reset)
(
module otwayrees
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 -> nonce -> {S : princ} ltk A S -> state.
ORRule1:
 forall Kas : ltk A S.
  empty => 
  exists M : nonce.
  exists Na : nonce.
  net(M & A & B & enc Kas (Na & M & A & B)), LA M Na S Kas.

ORRule5:
   forall Kas : ltk A S.
   forall Kab : stk A B.
   forall M : nonce.
   forall Na : nonce.
   net(M & enc Kas (Na & Kab)), LA M Na S Kas
     => empty.
--- when the L wasnt declared, Na declaration with forall wasnt necessary...but after that..reconstruction was not possible. 

}


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

ORRule4:
   forall Kas : ltk A S.
   forall Kab : stk A B.
   forall Kbs : ltk B S.
   forall M : nonce.
---   forall Na : nonce.
  forall Nb : nonce.
   net(M & enc Kas (Na & Kab) & enc Kbs (Nb & Kab)), LB M Nb S Kbs
 => net(M & enc Kas (Na & Kab)).

}


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

}

)
 

Findings

Reconstruction not possible to large extent, thus the variables needed to be defined using forall in most cases.