\documentclass[letterpaper,english,10pt]{llncs}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\setlength\parskip{\medskipamount}
\setlength\parindent{0pt}
\usepackage{babel,url}
\begin{document}
\title{Mondex with the Alloy model-finding method}
\author{Tahina Ramananandro\inst{1} \and Daniel Jackson\inst{2}}
\institute{\'Ecole Normale Sup\'erieure, 75005 Paris (France) \\
\url{http://www.eleves.ens.fr/~ramanana/work/mondex} \and
  Massachusetts Institute of Technology, Cambridge MA 02139 (USA) \\ \url{http://alloy.mit.edu}}
\maketitle

\textbf{Specifying Mondex with the Alloy specification language.} Starting
from the existing specification in Z, we wrote a specification of Mondex in
the Alloy specification language, based on relational first-order logic
with transitive closures.

There is no notion of records, so, contrary to Z, Alloy does not need
$NAME$s to disambiguate two objects having the same field values.

We have chosen to represent amounts through sets of coins. So, we modelled
a system similar to physical coins instead of integers. We had to develop
constraints to prevent purses from sharing common coins in their balances.
Then, values can be computed through relational operators gathering the
corresponding coins.

But infiniteness cannot be expressed with the Alloy logic, so all those
issues have been dropped in our work.

If finiteness issues are dropped, then it is worth noting that the Mondex
specification can be expressed in first-order logic even without transitive
closures.


\textbf{Checking the model with Alloy Analyzer, a model finder.} We checked
the specification with Alloy Analyzer, a piece of software developed by the
Software Design group at MIT and based on model-finding : it translates the
model into a boolean formula which it tries to satisfy.  If an assignment
of variables is found, then the program translates it back to get a
counterexample.

However, such a translation is possible only for a predefined scope, that
is given a finite bound on the number of objects in an instance. The model
has been checked for a scope of at most 8 objects per kind (8 coins, 8
purses, \dots) but considering only the relevant pre-states and post-states
for each operation.

Counterexamples allowed us to find the following bugs :

\begin{itemize}
\item Purses can hold unauthentic transaction details.
\item Wrong case analysis in the proof of the Abort/AbIgnore refinement.
\item The $\Phi BOp$ framing schema does not take the $ether$ into
  account.
\end{itemize}

\textbf{Further work.} The Alloy model-finding method is useful to find
bugs in the specification ; however, it provides no proof. But it could be
interesting to get first-order theories from the Alloy model and submit
them to automated theorem provers. However, first attempts gave quite few
results : only theorems relevant to the Abstract world security properties
have been proved.

\end{document}