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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.