BAN Inference Rules
These inferences are supposed to be valid despite attacker interference.
(1) Message-meaning rules
P bel Q <-K-> P, P sees {X}K |– P bel Q said X
P bel K-> Q, P sees {X}K-1 |– P bel Q said X
P bel Q <-Y-> P, P sees Y |– P bel Q said X
P bel fresh(X), P bel Q said X |– P bel Q bel X
P bel Q controls X, P bel Q bel X |– P bel X