More BAN Rules

(4) Sees rules

P sees (X, Y) |– P sees X, P sees Y

P sees Y |– P sees X

P bel Q <-K-> P, P sees {X}K |– P sees X

P bel K-> P, P sees {X}K |– P sees X

P bel K-> Q, P sees {X}K -1 |– P sees X

(5) Freshness

P bel fresh(X) |– P bel fresh(X, Y) (inside encryption)

• Symmetry of <-K-> and <-X-> is implicitly used

• Conjunction is handled implicitly

  P bel (X, Y) |– P bel X and P bel Y
  
  P bel Q said (X, Y) |– P bel Q said X, P bel Q said Y

Previous slide

Next slide

Back to first slide

View graphic version