theory BKE
begin

section{* Bilateral Key Exchange with Public Key protocol (BKEPK) *}

text{*
  Modeled after the description 6.6.6 in the Clark-Jacob library:

   http://www.csl.sri.com/users/millen/capsl/library2.html

 Notable differences:

   1. We are using explicit global constants to identify the different
      encryptions instead of implicit typing.

*}

protocol BKE {
  1. I -> R: I, { 'TT1', ni, I }pk(R)
  2. I <- R: { 'TT2', h(ni), nr, R, kir }pk(I)
  3. I -> R: { 'TT3', h(nr) }kir
}

subsection{* Secrecy Properties *}

properties (of BKE)
  // type invariant inferred from the protocol specification
  auto: msc-typing

  // originated terms secrecy
  I_ni_secrecy:   secret(I, -, ni,    {I,R}) 
  R_nr_secrecy:   secret(R, -, nr,    {I,R}) 
  R_kir_secrecy:  secret(R, -, kir,   {I,R}) 

  // composed originated terms secrecy
  I_hash_ni_secrecy: secret(I, -, h(ni),  {I,R}) 
  R_hash_nr_secrecy: secret(R, -, h(nr),  {I,R}) 

  // variable secrecy
  I_nr_secrecy:   secret(I, 2, nr,    {I,R}) 
  I_kir_secrecy:  secret(I, 2, kir,   {I,R}) 
  R_ni_secrecy:   secret(R, 3, ni,    {I,R}) 


subsection{* Authentication Properties *}

property (of BKE) 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
     & kir#1 = kir#2
     &   St(1,I_1) < St(2,R_1) 
       < St(2,R_2) < St(1,I_2) 
       < St(1,I_3)"

property (of BKE) 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
     & kir#1 = kir#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