2
$\begingroup$

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

$\endgroup$
4
  • $\begingroup$ This looks like someone wrote basic deductive logic in an alien language. $\endgroup$
    – Mario Carneiro
    Oct 13, 2015 at 6:46
  • 1
    $\begingroup$ Your guess is correct. $\endgroup$
    – MJD
    Oct 14, 2015 at 14:52
  • $\begingroup$ @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. $\endgroup$
    – Celeritas
    Oct 14, 2015 at 21:33
  • $\begingroup$ @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. $\endgroup$
    – Mario Carneiro
    Oct 14, 2015 at 23:02

1 Answer 1

Reset to default
5
$\begingroup$

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

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .