theory Yahalom2
begin

section{* The Yahalom Protocol, Variant 2 *}

text{*
  Modelled according to Paulson's variant of the Yahalom protocol in
  Isabelle/src/HOL/Auth/Yahalom2.thy. Instead of assuming a typed model we are
  using global constants to ensure distinctness of messages from different
  steps.

  We do not model session key leakage. Once we have incorporated dynamically
  compromosing adversaries into the proof generation algorithm, this will be
  modeled precisely.
*}

protocol yahalom_paulson
{
   1. I -> R: I, ni

   2. R -> S: R, nr, {'TT1', I, ni}k(R,S)

   3.   <- S: S, nr, {'TT31', R, kir, ni}k(I,S), {'TT32', I, kir, nr}k(R,S)
      I <-  : S, nr, {'TT31', R, kir, ni}k(I,S), Ticket

   4. I ->  : Ticket,                     {'TT4', nr}kir
        -> R: {'TT32', I, kir, nr}k(R,S), {'TT4', nr}kir

}


subsection{* Secrecy Properties *}

properties (of yahalom_paulson)
  S_kir_sec: secret(S, -, kir, {I,R,S})
  I_kir_sec: secret(I, 3, kir, {I,R,S})
  R_kir_sec: secret(R, 4, kir, {I,R,S})


subsection{* Authentication Properties *}

property (of yahalom_paulson) I_ni_synch:
  premises
    "role(1) = I"
    "step(1, I_3)"
    "uncompromised(I#1, R#1, S#1)"
  imply threads 2 ,3 such that
    "  role(2) = R
     & role(3) = S
     & I#1  = I#2   & I#2  = I#3
     & R#1  = R#2   & R#2  = R#3
     & ni#1 = ni#2  & ni#2 = ni#3
     & kir#1 = kir#3               // we are not guaranteed that responder received kir
     &   St(1,I_1) < St(2,R_1) 
       < St(2,R_2) < St(3,S_2) 
       < St(3,S_3) < St(1,I_3)"

property (of yahalom_paulson) R_ni_synch:
  premises
    "role(2) = R"
    "step(2, R_4)"
    "uncompromised(I#2, R#2, S#2)"
  imply threads 1 ,3 such that
    "  role(1) = I
     & role(3) = S
     & I#1  = I#2   & I#2  = I#3
     & R#1  = R#2   & R#2  = R#3
     & nr#1 = nr#2  & nr#2 = nr#3
     // no agreement over ni because it is not bound to nr
     // & ni#1 = ni#2  & ni#2 = ni#3
     & kir#1 = kir#2 & kir#2 = kir#3
     &               St(2,R_1) 
       < St(2,R_2) < St(3,S_2) 
       < St(3,S_3) < St(1,I_3)
       < St(1,I_4) < St(2,R_4)"

end