theory BrandsChaum
begin

section{* Distance bounding following Brands, Chaum *}

text{*

We model the distance bounding protocol following Brands and Chaum

  Stefan Brands and David Chaum. Distance-Bounding Protocols. EUROCRYPT '93     
  Lecture Notes in Computer Science 765, pp. 344--359, Springer, 1993.

Since the Dolev-Yao model has no notion of time, we can only show that
the challenge-response steps have to happen in the right order.

*}

protocol BrandsChaum
{
  1. P ->   : P, {m}k
       -> V : P, c
  2. P <- V : a
  3. P ->   : h(a, m)
       -> V : b
  4. P ->   : m, k, {a, h(a, m)}sk(P)
       -> V : m, k, {a, b}sk(P)
  5.      V : c -> {m}k
  6.      V : b -> h(a, m)
}

property (of BrandsChaum) prover_recent:
  premises
    "role(0) = V"
    "step(0, V_6)"
    "uncompromised(P#0)"
  injectively imply a thread 1 such that
    "role(1) = P &
    P#0 = P#1 &
    m#0 = m#1 &
    k#0 = k#1 &
    a#0 = a#1 &
    St(1, P_1) < St(0, V_2) < St(1, P_3) < St(0, V_3)
    "

end