\documentstyle{article}
\begin{document}

\newcommand{\believes}{\;|\!\smash{\equiv}\;}
\newcommand{\said}{\;|\!\smash{\sim}\;}
\newcommand{\sees}{\triangleleft}
\newcommand{\jurisdiction}{\;|\!\smash{\Rightarrow}\;}
\newcommand{\fresh}{\sharp}
\newcommand{\encrypted}[2]{\{ #1 \}_{#2}}

\begin{center}{\bf\Large
A simple authorization protocol
}\\{\em
Burton Rosenberg\\
University of Miami
}\end{center}


\abstract
{
We present an authorization protocol designed around the
assumptions of a thin-client.
The client does not need to generate random values, keep
time or hold state.
The protocol uses symmetric key encryption and a central
key repository and permissions manager.
Services are assured the identity
and authorization of the user for the requested service.
Users have some assurances concerning the action performed on their
behalf. The protocol is presented and formally analyzed.
The limitations of the assurances made to the user are
discussed.
}

\subsection*{Introduction}

We present an authorization protocol designed around the assumptions
of a thin-client. In particular, we assume
that the client does not have access to high quality
random values, that it does not keep reliable time, and that
it is inconvenient for it to hold state or to be personalized with
user specific data. A typical scenario would be a small computer 
equiped with a SmartCard reader and a Web browser.
Using the browser, the user converses with the service
in an informal way and agrees upon an action.
The protocol then provides for a central permissions manager to authorize
the action and assures the service and the permissions manager
of the identity of the user. The protocol requires four messages,
only two of which involve the client.

While there is much in common with the classical authentication using
symmetric key encryption, such as Needham-Schroeder
\cite{needham_schroeder_1978,needham_schroeder_1987},
Otway-Rees \cite{otway_rees_1987}, and
Kerberos \cite{kerberos}, this protocol is designed 
to be light weight, but does not achieve all that these
protocols achieve. In particular, the user does not authenticate
the service, and is therefore useful only in situations of
asymmetric trust relations. Such is the case, for instance, in
the permission to access a printer. A user hardly ever complains
about being given gratuitous permission to a printer, whereas the
printer's owner generally wants controls.

The protocol uses symmetric key encryption. The authentication
system could be incoporated in freeware products, and therefore
needs to avoid expensive or legally encombered cryptographic products.
Since in any case the system must refer to a central 
permission mananger to grant actions and accept liability,
the inconveniences of symmetric key are offset by 
a transparent legal structure.

The protocol is presented 
in the next section. Following we transform and
analyze the protocol using BAN logic
\cite{burrows_abadi_needham_1989}.
We conclude with a discussion of the limitations of this protocol.

\subsection*{Description}

Our protocol is diagramed in Figure~\ref{protocol_figure}.
Let $U, S$ and $T$ represent the user, service and a trusted third
party, respectively. The trusted third party functions as the
permissions manager and shares keys with $U$ and $S$.
After a conversation between $U$ and $S$, $U$ requests action $A$.
The service $S$ tags the request with an identifier $I$ and forwards it
to $T$ for authorization. If $T$ authorizes the request, it generates
a session key $K$, a timestamp $t$, and an authorization nonce $N$.
It sends the reply $Q=\encrypted{U, S, A, N, t}{K}$,
where $\encrypted{R}{K}$ denotes message $R$ encrypted and
integrity protected with the symmetric key $K$.
The service will forward
a copy of $Q$ to $U$, along with $\encrypted{K}{U}$, and await the return of
$N$ in clear. If $U$ does not agree that it asked $A$ of $S$, it will not
echo $N$. If $t$ has expired, $S$ will not honor the returned $N$.

\newcommand{\theWidth}{2.3cm}
\begin{figure}
\begin{center}
\begin{tabular}{c|ccc|ccc|c}
\multicolumn{2}{c}{$U$} & \makebox[\theWidth]{} 
   & \multicolumn{2}{c}{$S$} & \makebox[\theWidth]{} & \multicolumn{2}{c}{$T$} \\
&&
   \leftarrowfill ~etc \rightarrowfill &&&&& \\
&&
 \rightarrowfill &&& \rightarrowfill && \\
 &&
   $A$ &&&  $(I,U,S,A)$ &&\\
&& &&& \leftarrowfill && \\
&& &&& $(I,\encrypted{K}{U}, \encrypted{K}{S}, Q) $ && \\
&& \leftarrowfill &&& && \\
&& $(\encrypted{K}{U},Q)$ &&& && \\
&& \rightarrowfill &&& && \\
&& $N$ &&& && \\
\end{tabular}
\end{center}
\caption{A simple authentication protocol\label{protocol_figure}}
\end{figure}

\subsection*{Analysis of protocol}

The protocol is analyzed using the method of Burrows, et. al.
\cite{burrows_abadi_needham_1989}.
The notation is reviewed in the Appendix.
Formalized, the protocol is reduced to three messages:
\begin{enumerate}
\item 
   $T\longrightarrow U: \encrypted{M,N}{U}$.
\item
   $T\longrightarrow S: \encrypted{t, N, 
        (U\said N \Rightarrow U \believes M)}{S}$.
\item
   $U\longrightarrow S: N$.
\end{enumerate}
The request $M$ reads: $U$ wants $S$ to do $A$.
The permission $N$ reads: $T$ allows that $S$ does $A$ for $U$.
In the formalization, $U$ and $S$ receive these messages unsolicited.
The goal of the protocol is $U,S\believes N,M$.

Our axioms are:
\begin{enumerate}
\item
  $U \believes M$, else abort protocol.
\item
  $S\believes U \jurisdiction M$.
\item  
  $U \believes \fresh{M}$.
\item
  $S \believes \fresh{t}$.
\item
  $S \believes T \jurisdiction (U\said N \Rightarrow U \believes M)$.
\item
  $U, S \believes T \jurisdiction N$.
\item
  $U \believes U {U\atop \longleftrightarrow} T$.
\item
  $S \believes S {S\atop \longleftrightarrow} T$.
\item
  $S \believes U { X \atop \longleftrightarrow} S$ for secrets $X$
  shared only by $U$, $S$ and $T$.
\end{enumerate}
The calculation for $U$ is not surprising, but it does use the freshness of $M$,
\begin{eqnarray*}
U \sees \encrypted{M,N}{U}, \; 
U \believes U {U\atop \longleftrightarrow} T
& \Rightarrow &
U \believes T\said{(M, N)}\\
& & \\
U \believes T\said{(M, N)}, \;
U \believes \fresh{M}
  &\Rightarrow&
U \believes T\believes (M,N).   \\
& & \\
U \believes T\believes (M,N), \;
U \believes T \jurisdiction N,
  &\Rightarrow &
U \believes N.  \\ 
\end{eqnarray*}
The calculation for $S$ is more involved. Using the freshness of $t$,
we find:
\[
S \believes T \believes (t, (U\said N \Rightarrow U\believes M), N).
\]
Using the the belief of $S$ of the jurisdiction of $T$, we conclude:
\[
S \believes (U\said N \Rightarrow U \believes M), N.
\]
With the arrival of $N$ to $S$:
\begin{eqnarray*}
S \sees N \mbox{ from } U,
\;
S \believes U {X \atop \longleftrightarrow} S \mbox{ for } N
  &\Rightarrow&
S \believes U \said N. \\
& & \\
S \believes (U \said N \Rightarrow U \believes M),
\; S \believes U \said N
&\Rightarrow& S \believes U \believes M \\
& & \\
S \believes U \believes M,
\; S \believes U \jurisdiction M
&\Rightarrow& S\believes M. \\
\end{eqnarray*}
Hence we conclude $U,S\believes M,N$.

\subsection*{Conclusions}

This protocol has the unique advantage of requiring little of the
client. However, an important limitation must be noted.

Since a client machine stands between
the user and the client, the client machine can hold two conversations, 
one with the service the user desires, and a second with a service 
the client desires, showing the user only one of the conversations, 
and the client the other. In formal terms, how can the user and client
know that they share $S$ and $A$ before releasing $N$?

Even with no further improvements, this weakness is mitigated by
the fact that the permissions manager holds a complete
paper trail of any such deceit and can attempt a roll-back of damages
once the deceit is detected.
A more complete solution is left for future research.

\appendix
\subsection*{Appendix}

We collect the notation and inference rules for BAN logic.
\[
\begin{array}{ll}
A \believes N & \mbox{$A$ believes $N$} \\
A \said N & \mbox{$A$ has said $N$} \\
A \sees N \mbox{\em from } B& \mbox{$A$ sees $N$ from $B$} \\
\sharp{N} & \mbox{$N$ is fresh} \\
A {K\atop \longleftrightarrow} B & 
   \mbox{$A$ and $B$ share secret key $K$} \\
\encrypted{N}{K} & \mbox{$N$ is encrypted and integrity protected with $K$} \\
A \jurisdiction N & \mbox{$A$ has jurisdiction over $N$}
\end{array}
\]
The message-meaning rule:
\[
\mbox{If } A\sees \encrypted{N}{K} \mbox{ from } B \mbox{, and }
A\believes A{K\atop \longleftrightarrow} B
\mbox{, then } A\believes B \said N.
\]
The nonce-verification rule:
\[
\mbox{If } A\believes B \said N \mbox{, and } A\believes \fresh{N}
\mbox{, then } A\believes B\believes N.
\]
The jurisdiction rule:
\[
\mbox{If } A\believes B\believes N \mbox{, and }A\believes B \jurisdiction N
\mbox{, then } A\believes N.
\]

\begin{thebibliography}{99}

\bibitem{needham_schroeder_1978}
Roger Needham, Schroeder, M. D., {\em Using encryption for authentication in large
networks of computers,} Comm. of the ACM, Vol. 21. No 12., pp. 993--999,
1978.

\bibitem{needham_schroeder_1987}
Roger Needham, Schroeder, M. D., {\em Authentication revisited,}
Op. Sys. Review, Vol.  21, No. 1 p, 7. 1987.

\bibitem{otway_rees_1987}
Otway, D., Rees, O. {\em Efficient and timely mutual authentication,}
Op. Sys. Review, Vol 21, No. 1 pp 8--10. 1987.

\bibitem{kerberos}Miller, S. P., Neuman, C., Schiller, J. I., Saltzer, J. H.,
{\em Kerberos authentication and authorization systems,} Proj. Athena Tech. Plan,
Section E.2.1., MIT, 1987.

\bibitem{burrows_abadi_needham_1989}
Michael Burrows, Martin Abadi, Roger Needham, {\em A logic of authentication,}
SRC Research Report 39, DEC. 1989.

\end{thebibliography}

\end{document}
