CR_paper.spthy

theory CR_Paper
begin

section{* The Running Example of Our CSF'10 Paper *}

protocol CR 
{
  1. C -> S: {k}pk(S)
  2. C <- S: h(k)
}

properties (of CR) 
  C_k_secrecy:    secret(C, -, k, {S} )

property (of CR) C_ni_synch:
  premises
    "role(1) = C"
    "step(1, C_2)"
    "uncompromised(S#1)"
  imply a thread 2 such that
    "  role(2) = S
     & S#1  = S#2
     & k#1 = k#2
     &   St(1,C_1) < St(2,S_1) 
       < St(2,S_2) < St(1,C_2)"

end