Analysis

  

Figure 1: Messages in the protocol.

The protocol consists of three messages, as illustrated in Figure 1. The messages are explicit, and contain sufficient information that their meaning can be established without context. That is, the meaning of messages does not depend on a (set of) previous message(s).

A BAN logical analysis of the protocol begins with the observation that Message 1 (denoted X in the protocol description) is received by B over a ``real time'' channel, implying that $B \vert\equiv \sharp(X)$ (see [1]). The assumption $B \vert\equiv \stackrel{K_A}{\mapsto} A$makes it possible for B to believe that $A \vert\sim X$; a similar argument also holds for S. If B believes that S is honest [16], we obtain $B \vert\equiv S \vert\equiv \textrm{data}$ because $B \vert\equiv \sharp(X)$and $B \vert\equiv S \vert\sim (X \textit{data})$(derived from Message 3). In other words, B believes that he has received the correct file from S.

At a higher level [9], Message 1 contains two statements (we only deal with reading, writing is similar):

$$A~\textbf{says}~B\vert A \Rightarrow B~\textbf{for}~A \eqno{(1)}$$

and

$$A~\textbf{says}~B~\textbf{for}~A~\textit{may read file F}{.}\eqno{(2)}$$

Statement (1) says says that the combined principal B|A may speak for B for A, while (2) says that B for A may read from file F. When B includes Message 1 in Message 2, it is interpreted as

$$B\vert A~\textbf{says}~\textit{read F}{.}\eqno{(3)}$$

Statement (3) enables S to deduce that B (by quoting A) indeed speaks for B for A. Consequently, if A owns the file F, then (3) should be honored.