theory OtwayRees
begin

section{* The Original Otway-Rees Protocol *}

text{*
  Based on Paulson's model in Isabelle/src/HOL/Auth/OtwayRees.thy. Notable
  differences:

    1. Instead of implicit typing, we are using explicit global constants to
       differentiate between different encryptions.

    2. We do not model session key compromise, as our key compromise
       infrastructure is not ready yet.
*}

protocol OtwayRees
{
  1. I ->  : ni, I, R, {'TT1', ni, I, R}k(I,S)
       -> R: ni, I, R, Ticket1
  2. R ->  : ni, I, R, Ticket1,                 {'TT2', ni, nr, I, R}k(R,S)
       -> S: ni, I, R, {'TT1', ni, I, R}k(I,S), {'TT2', ni, nr, I, R}k(R,S)

  3.   <- S: ni, {'TT3', ni, kIR}k(I,S), {'TT3', nr, kIR}k(R,S) 
     R <-  : ni, Ticket2,                {'TT3', nr, kIR}k(R,S) 
  4.   <- R: ni, Ticket2
     I <-  : ni, {'TT3', ni, kIR}k(I,S)
}


subsection{* Secrecy Properties *}

properties (of OtwayRees)
  S_kIR_sec: secret(S, -, kIR, {I,R,S})
  R_kIR_sec: secret(R, 3, kIR, {I,R,S})
  I_kIR_sec: secret(I, 4, kIR, {I,R,S})


subsection{* Authentication Properties *}

property (of OtwayRees) ni_first_send:
  premises
    "role(1) = I"
    "knows(ni#1)"
  imply "St(1, I_1) < Ln(ni#1)"

text{*
  Note that the guarantees would be way better, if we the initiator would
  receive an unfakeable message from the responder after he received the
  session key. Currently, we just don't have a means to check that the
  responder received the servers message. Hence, we cannot prove agreement on
  'kIR'.
*}
property (of OtwayRees) I_auth:
  premises
    "role(1) = I"
    "uncompromised(I#1, R#1, S#1)"
    "step(1, I_4)"
  imply threads 2, 3 such that
    " 
      role(2) = R &
      role(3) = S &

      I#1 = I#3 &
      R#1 = R#3 &
      S#1 = S#3 &
      ni#1 = ni#3 &
      kIR#1 = kIR#3 &

      I#1 = I#2 &
      R#1 = R#2 &
      S#1 = S#2 &
      ni#1 = ni#2 &

      nr#2 = nr#3 &

      //ordering
      St(1, I_1) < St(2, R_1) <
      St(2, R_2) < St(3, S_2) <
      St(3, S_3) < St(1, I_4)
    "

property (of OtwayRees) R_ni_agree:
  premises
    "role(2) = R"
    "uncompromised(I#2, R#2, S#2)"
    "step(2, R_3)"
  imply threads 1, 3 such that
    " 
      role(1) = I &
      role(3) = S &

      I#2 = I#1 &
      R#2 = R#1 &
      S#2 = S#1 &
      ni#2 = ni#1 &

      I#2 = I#3 &
      R#2 = R#3 &
      S#2 = S#3 &
      ni#2 = ni#3 &
      nr#2 = nr#3 &
      kIR#2 = kIR#3 &

      //ordering
      St(1, I_1) < St(2, R_1) <
      St(2, R_2) < St(3, S_2) <
      St(3, S_3) < St(2, R_3)
    "

text{*
  Comparing the proofs of S_ni_agree and R_ni_agree we see that they are pretty
  similar. We have yet to find the right formulation that allows to share the
  similar subproofs.
*}

property (of OtwayRees) S_ni_agree:
  premises
    "role(3) = S"
    "uncompromised(I#3, R#3, S#3)"
    "step(3, S_2)"
  imply threads 1, 2 such that
    " 
      role(1) = I &
      role(2) = R &

      I#2 = I#1 &
      R#2 = R#1 &
      S#2 = S#1 &
      ni#2 = ni#1 &

      I#2 = I#3 &
      R#2 = R#3 &
      S#2 = S#3 &
      ni#2 = ni#3 &
      nr#2 = nr#3 &

      //ordering
      St(1, I_1) < St(2, R_1) <
      St(2, R_2) < St(3, S_2)
    "

end