I'm learning BAN logic and trying to understand the notation. The bellow picture is an example form Security Engineering by Ross J Anderson. My question is what does the horizontal line mean? I'm guessing it can be read like and if/then statement where the top is the if condition and bottom is the then part? Also I guess the comma (,) means "and"?
the nonce-verification rule thates that if a principal once said a message, and the message is fresh, then that principal still believes it. Formally,
$$\frac{A\mid\equiv\sharp X, \quad A\mid\equiv B\mid\sim X}{A\mid\equiv B\mid\equiv X}.$$
Best Answer
This is a deduction from two statements to a third one. $A\mid\equiv B$ is read "$A$ believes $B$", $\sharp X$ is read "$X$ is fresh", and $A\mid\sim X$ is read "$A$ (once) said $X$". The operator $\mid\equiv$ is right associative, so $A\mid\equiv B\mid\equiv X$ is parsed as $A\mid\equiv (B\mid\equiv X)$ and $A\mid\equiv B\mid\sim X$ is parsed as $A\mid\equiv (B\mid\sim X)$.
The statement in question says: Suppose that in the course of a proof we have derived $A\mid\equiv\sharp X$, meaning that we have proven that $A$ believes $X$ is fresh, and we have also derived $A\mid\equiv B\mid\sim X$, meaning that we have proven that $A$ believes $B$ said $X$. Then we are allowed to deduce the statement $A\mid\equiv B\mid\equiv X$, that is, $A$ believes that $B$ believes $X$.
An inference rule like this is traditionally written with a "fraction bar" notation such as
$$\frac{A\mid\equiv\sharp X\qquad A\mid\equiv B\mid\sim X}{A\mid\equiv B\mid\equiv X}.$$
A propositional logic version that you may be more familiar with is modus ponens: If $P$ is provable and $P\to Q$ is provable, then $Q$ is provable. This rule might be written as:
$$\frac{P\quad P\to Q}{Q}.$$