# BAN logic notation: what does horizontal line mean?

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}.$$

• This looks like someone wrote basic deductive logic in an alien language. – Mario Carneiro Oct 13 '15 at 6:46
• Your guess is correct. – MJD Oct 14 '15 at 14:52
• @MJD thanks, sometimes a simple 'yes' is better than a long winded explanation that muddles the simplicity of the answer. I would say if you post this as an answer I'd accept it but I guess it's too short to be allowed. – Celeritas Oct 14 '15 at 21:33
• @Celeritas The reason why I went for the "long winded explanation" instead of just saying "yes" is because the description of a deduction as an if/then is not quite correct and confuses meta-levels. It is an if/then outside the language, from one provable assertion to another, by contrast to if-thens inside the language such as the "$P\to Q$" in my example. – Mario Carneiro Oct 14 '15 at 23:02

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$.
$$\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}.$$