Table 1. BAN logic rules.

Rule	Description
P ⊲ X	P receives a message containing X
P \| ~ X	P sends a message containing X
P \| ≡ X	P believes X
P ↔ K Q	P and Q share secret K
< X > Y	X contains the secret Y
P ⇒ X	P has the right to decide whether X is right or not
Message meaning rule	P \| ≡ P ↔ K Q , P ⊲ < X > Y P \| ≡ Q \| ~ X
Belief rule	P \| ≡ X , P \| ≡ Y P \| ≡ ( X , Y )
Nonce verification rule	P \| ≡ # ( X ) , P \| ≡ Q \| ~ X P \| ≡ Q \| ≡ X
Arbitration rule	P \| ≡ Q ⇒ X , P \| ≡ Q \| ~ X P \| ≡ X