theory AndrewRPC begin

section{* Andrew Secure RPC *}

text{*
  We do not have the original model of the Isabelle/OFMC AndrewRPC protocol.
  Therefore, we orient ourself on the SPORE library model.

  Notable differences:

    1. Instead of implicit typing, we are using explicit global constants to
       discern messages.
*}

protocol Andrew {

  1. I -> R: I, { 'TT1', ni }k(I,R)
  2. I <- R: { 'TT2', h('TT1', ni), nr }k(I,R)
  3. I -> R: { 'TT3', h('TT1', nr) }k(I,R)
  4. I <- R: { 'TT4', kIR, nr2 }k(I,R)

}


subsection{* Security Properties *}

properties (of Andrew)
  R_sec_kIR: secret(R, -, kIR, {I, R})
  I_sec_kIR: secret(I, 4, kIR, {I, R})


property (of Andrew) I_ni_agree:
  premises
    "role(1) = I"
    "step(1, I_4)"
    "uncompromised(I#1,R#1)"
  imply a thread 2 such that
    "  role(2) = R
     & I#1  = I#2
     & R#1  = R#2

     // These commented out equalities don't hold because there may be another
     // thread having sent the initial message exchange. Put differently: the
     // protocol is missing a link between nr,ni and nr2,kIR.
     // & ni#1 = ni#2
     // & nr#1 = nr#2

     & nr2#1 = nr2#2
     & kIR#1 = kIR#2 "

property (of Andrew) R_ni_agree:
  premises
    "role(1) = R"
    "step(1, R_4)"
    "uncompromised(I#1,R#1)"
  imply a thread 2 such that
    "  role(2) = I
     & I#1  = I#2
     & R#1  = R#2
     & ni#1 = ni#2
     & nr#1 = nr#2"
     // here we don't have agreement on the key because 'R' cannot check if it
     // has been received.

end