theory NS_Public
begin

section{* The Needham-Schroeder-Lowe Public-Key Protocol *}

text{*
  Modeled after the description by Paulson in Isabelle/HOL/Auth/NS_Public.thy.

  Notable differences:
    
    1. We are using explicit global constants for discerning the different
       encryption instead of the implicit typing.
*}


protocol ns_public
{
  1. I -> R: {'1',ni,I}pk(R)
  2. I <- R: {'2',ni,nr,R}pk(I)
  3. I -> R: {'3',nr}pk(R)
}


subsection{* Secrecy Properties *}

properties (of ns_public) 
  I_ni_secrecy:   secret(I, -, ni, {I,R}) 
  R_nr_secrecy:   secret(R, -, nr, {I,R}) 
  I_nr_secrecy:   secret(I, 2, nr, {I,R}) 
  R_ni_secrecy:   secret(R, 3, ni, {I,R}) 


subsection{* Authentication Properties *}

property (of ns_public) I_ni_synch:
  premises
    "role(1) = I"
    "step(1, I_3)"
    "uncompromised(I#1, R#1)"
  imply a thread 2 such that
    "  role(2) = R
     & I#1  = I#2
     & R#1  = R#2
     & ni#1 = ni#2
     & nr#1 = nr#2
     &   St(1,I_1) < St(2,R_1) 
       < St(2,R_2) < St(1,I_2) 
       < St(1,I_3)"

property (of ns_public) R_ni_synch:
  premises
    "role(1) = R"
    "step(1, R_3)"
    "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
     &   St(2,I_1) < St(1,R_1) 
       < St(1,R_2) < St(2,I_2) 
       < St(2,I_3) < St(1,R_3)"


end