WooLam.spthy

theory WooLam
begin

section{* Woo and Lam Mutual Authentication Protocol *}

text{*
  Modeled after the description in the SPORE library:

    http://www.lsv.ens-cachan.fr/Software/spore/wooLamMutual.html

  Notable differences:

    1. We are using explicit global constants to discern between different
       encryptions instead of the implicit typing, which introduces
       ambiguities. This implies that we are not precisely modeling the Woo and
       Lam protocol of the SPORE library and hence we may miss some attacks
       possible on it. However, every implementation of the SPORE model could
       easily be changed to our version and benefit from the full correctness
       proof.
*}

protocol WooLam
{
  1. A -> B: A, na
  2. A <- B: B, nb
  3. A ->  : {'enc3', A, B, na, nb}k(A,S)
       -> B: Ticket1
  4. B ->  : Ticket1,                      {'enc4', A, B, na, nb}k(B,S)
       -> S: {'enc3', A, B, na, nb}k(A,S), {'enc4', A, B, na, nb}k(A,S)
  5.   <- S: {'enc51', B, na, nb, kab}k(A,S), {'enc52', A, na, nb, kab}k(B,S)
     B <-  : Ticket2,                         {'enc52', A, na, nb, kab}k(B,S)
  6.   <- B: Ticket2,                         {'enc6', na,nb}kab
     A <-  : {'enc51', B, na, nb, kab}k(A,S), {'enc6', na,nb}kab
  7. A -> B: {'enc7', nb}kab
}


subsection{* Secrecy Properties *}

properties (of WooLam)
  S_sec_kab: secret(S, -, kab, {A,B,S})
  A_sec_kab: secret(A, 6, kab, {A,B,S})
  B_sec_kab: secret(B, 5, kab, {A,B,S})

  A_sec_inv_kab: secret(A, 6, inv(kab), {A,B,S})
  B_sec_inv_kab: secret(B, 5, inv(kab), {A,B,S})


subsection{* Authentication *}

property (of WooLam) na_first_send:
  premises
    "role(1) = A"
    "knows(na#1)"
  imply "St(1, A_1) < Ln(na#1)"

property (of WooLam) nb_first_send:
  premises
    "role(1) = B"
    "knows(nb#1)"
  imply "St(1, B_2) < Ln(nb#1)"

property (of WooLam) A_ni_synch:
  premises
    "role(1) = A"
    "uncompromised(A#1, B#1, S#1)"
    "step(1, A_6)"
  imply threads 2, 3 such that
    " role(2) = B &
      role(3) = S &

      A#1 = A#2 &
      B#1 = B#2 &
      S#1 = S#2 &
      na#1 = na#2 &
      nb#1 = nb#2 &
      kab#1 = kab#2 &

      A#1 = A#3 &
      B#1 = B#3 &
      S#1 = S#3 &
      na#1 = na#3 &
      nb#1 = nb#3 &
      kab#1 = kab#3 &

      //ordering
      St(1, A_1) < St(2, B_1) <
      St(2, B_2) < St(1, A_2) <
      St(1, A_3) < St(3, S_4) <
      St(3, S_5) < St(2, B_5) <
      St(2, B_6) < St(1, A_6) 
      & // we do not get a full ordering, because the ticket receive in B_3
        // does not give any guarantees.
                   St(2, B_3) <
      St(2, B_4) < St(3, S_4)
    "

property (of WooLam) B_ni_synch:
  premises
    "role(2) = B"
    "uncompromised(A#2, B#2, S#2)"
    "step(2, B_7)"
  imply threads 1, 3 such that
    " role(1) = A &
      role(3) = S &

      A#2 = A#1 &
      B#2 = B#1 &
      S#2 = S#1 &
      na#2 = na#1 &
      nb#2 = nb#1 &
      kab#2 = kab#1 &

      A#2 = A#3 &
      B#2 = B#3 &
      S#2 = S#3 &
      na#2 = na#3 &
      nb#2 = nb#3 &
      kab#2 = kab#3 &

      //ordering
      St(1, A_1) < St(2, B_1) <
      St(2, B_2) < St(1, A_2) <
      St(1, A_3) < St(3, S_4) <
      St(3, S_5) < St(2, B_5) <
      St(2, B_6) < St(1, A_6) <
      St(1, A_7) < St(2, B_7)
      & // we do not get a full ordering, because the ticket receive in B_3
        // does not give any guarantees.
                   St(2, B_3) <
      St(2, B_4) < St(3, S_4)
    "

property (of WooLam) S_ni_synch:
  premises
    "role(3) = S"
    "uncompromised(A#3, B#3, S#3)"
    "step(3, S_4)"
  imply threads 1, 2 such that
    " role(1) = A &
      role(2) = B &

      A#2 = A#1 &
      B#2 = B#1 &
      S#2 = S#1 &
      na#2 = na#1 &
      nb#2 = nb#1 &

      A#2 = A#3 &
      B#2 = B#3 &
      S#2 = S#3 &
      na#2 = na#3 &
      nb#2 = nb#3 &
      
      //ordering
      St(1, A_1) < St(2, B_1) <
      St(2, B_2) < St(1, A_2) <
      St(1, A_3) < St(3, S_4)
      & // we do not get a full ordering, because the ticket receive in B_3
        // does not give any guarantees.
                   St(2, B_3) <
      St(2, B_4) < St(3, S_4)
    "

end