An Audit Logic for Accountability (Extended Version\footnote{This is an extended version of the article to appear in the Conference Proceedings of the 6th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY 2005)} )
J.G. Cederquist$^1$
R. Corin$^1$
M.A.C. Dekker$^{1,2}$
S. Etalle$^1$ and J.I. den Hartog$^1$
[.1in] $^1$ Department of Computer Science
The Netherlands
[.1in] $^2$ Security Department
TNO ICT
%
ced05_full.tex
% General TODO
%       use macros for some things to guarantee consistency. (+ make existing macros consistent)
%       Add: remark about watermarking as method to recognize data.
%       Note that policy=usage policy=data (usage) policy. or use consistent naming

% \documentclass[oribibl,envcountsame,11pt,a4paper]{llncs}

%% kluwer document
%\documentclass[10pt]{article}
%\usepackage{a4wide}

\documentclass{article}
\usepackage{latex8}
\usepackage{times}
%\setlength{\paperwidth}{8.5in}
%\setlength{\paperheight}{11.5in}
%\setlength{\parindent}{.17in}
%\setlength{\columnsep}{.375in}  %.375in or .81cm ??
%\setlength{\textwidth}{6.5in}
%\setlength{\textheight}{9.875in}
%\topmargin -1in
\usepackage{epsfig,color}
%\usepackage{color,epsfig,graphicx,flafter}
\usepackage{amssymb,amsmath}
%\usepackage{latexsym,stmaryrd}
\newtheorem{proposition}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem}
\newtheorem{example}{Example}
\newtheorem{remark}{Remark}
\newtheorem{algorithm}{Algorithm}
\newtheorem{claim}{Claim}
\newenvironment{proof}{{\em Proof.}}{$\Box$}
%\usepackage{ifthen}
%%%%%%%%%%%%%%%
%% gabriele macro
%\usepackage{verbatim}
% syntactic symbols
\newcommand{\srd}{\mathsf{read}}
\newcommand{\ssay}{\;\mathsf{says}\;}
\newcommand{\sato}{\;\mathsf{to}\;}
\newcommand{\scom}{\mathsf{comm}}
\newcommand{\sown}{\; \mathsf{owns} \;}
\newcommand{\scre}{\mathsf{creates}}
\newcommand{\stime}{\mathsf{t}}

% SEMANTICS symbols
%\newcommand{\Scom}{\mathit{comm}}
%\newcommand{\Scre}{\mathit{create}}
%\newcommand{\Stime}{\mathit{t}}

% sets
%\newcommand{\Preds}{\mathcal{C}}  (replaced by Predicates)
%\newcommand{\agents}{\mathcal{G}} (replaced by Agents)
%\newcommand{\Data}{\mathcal{D}} (replaced by DataValues)

% semantics evidences
%\newcommand{\SEvids}{\mathcal{E}} (replaced by Evidences)

% syntactic evidences
%\newcommand{\sEvids}{\mathit{EV}}

% mapping of the evidences
%%\newcommand{\ev}[1]{e_{#1}}
%\newcommand{\ev}[1]{[{#1}]}

% meta symbols

% derivation tree
\newcommand{\dtree}{\mathcal{P}}

% implication
\newcommand{\impl}{\subset}

% step in a logical proof
%    2
%   --- 1
%    3
\newcommand{\lste}[3]{\cfrac{#2}{#3}_{\:\: #1}}

% step in a logical proof with label
%     3
%  1 --- 2
%     4
\newcommand{\llste}[4]{_{\tt #1} \: \cfrac{#3}{#4}_{\:\: #2}}

%% digit shortcut
\newcommand{\eg}{\emph{e.g., }}
\newcommand{\ie}{\emph{i.e., }}
\newcommand{\wrt}{\emph{w.r.t.~}}

%% marginal comments (m.c.)
\newcommand{\GTODO}[2][ic]
{$^{\fboxsep=1pt\fbox{\bf \tiny #1}}$%
 \marginpar{\fbox{\parbox[t]{\marginparwidth}{\tiny #2}}}}

\newcommand{\GCOMM}[2]{
$\blacktriangleright$
% $^{\fboxsep=1pt {\fbox{\bf  \tiny #1}}}$: %
{\bf  \tiny (#1)}:
{\tt \emph{#2}}$\blacktriangleleft$}

%% my personal m.c.
%% \newcommand{\mynote}[1]{\GTODO[*]{#1}}
\newcommand{\mynote}[1]{\GCOMM{g.}{#1}}
\newcommand{\mytodo}[1]{\GTODO[g.]{#1}}
\newcommand{\mytodor}[1]{\GTODO[r.]{#1}}

%%%%%%%%%%%%%%%%

\newcommand{\own}{\ \textsf{owns}\ }
\newcommand{\sent}{\textsf{sent}}
\newcommand{\comm}{\textsf{comm}}
\newcommand{\recv}{\textsf{received}}
\newcommand{\say}{\ \textsf{says} }
\newcommand{\creates}{\textsf{creates} }
\newcommand{\pol}{\ \textsf{policy}}
\newcommand{\cond}{\mathcal{C}}
\newcommand{\act}{\mathcal{A}}
\newcommand{\ato}{\ \textsf{to}\ }
\newcommand{\has}{\textsf{has}}
\newcommand{\state}{\mathcal{S}}
\newcommand{\glob}{\mathcal{G}}
\newcommand{\GOT}[3]{{#3} @_{#1} {#2}}

\newcommand{\JUS}[2]{{\tt Jus}_{#1}(#2)}

%\newcommand{\AUT}[2]{{\tt Aut}_{#1}(#2)}
%\newcommand{\AUTS}[2]{{\tt AUTS}_{#1}(#2)}

\newcommand{\ACC}[2]{{\tt Acc}_{#1}(#2)}
\newcommand{\SynT}{\textsf{SynT}}
\newcommand{\SemT}{\textit{SemT}}
\newcommand{\Time}{\mathcal{T} }

%\newcommand{\DAC}[2]{{\tt Dac}_{#1}(#2)}
\newcommand{\GDAC}[2]{{\tt GDac}_{#1}(#2)}
\newcommand{\SDAC}[2]{\ensuremath{{\tt SDac}_{#1}(#2)}}
\newcommand{\EVSDAC}[2]{\ensuremath{{\tt EvSDac}_{#1}(#2)}}
\newcommand{\Nat}{\emph{Nat}}

\newcommand{\prf}[2]{{\cal P}\llbracket {\cal A}(#1) \vdash_{#1}
  #2\rrbracket}


%% Jerrys macros
\newcommand{\old}[1]{}                          % old text, hide.
\newcommand{\jtodo}[1]{\GTODO[j.]{#1}}          % comments
\newcommand{\jnote}[1]{\GTODO[*]{#1}}

\newcommand{\twocases}[4]{
  \left \lbrace
  \begin{array}{ll}
    #1 & \mbox{#2} \\
    #3 & \mbox{#4}
  \end{array}
  \right .
}

% Sets
\newcommand{\Agents}{\mathcal{G}}
\newcommand{\Var}{\mathcal{V}}
\newcommand{\DataValues}{\mathcal{D}}
\newcommand{\Predicates}{\mathcal{C}}           % \mathcal{P}}
\newcommand{\PolicyFormulae}{\Phi}
%\newcommand{\EvidenceFormulae}{\mathcal{E}}     % = \sEvids
%\newcommand{\EvidenceFormulae}{\mathit{EV}}
\newcommand{\Evidences}{\mathcal{E}}

% Syntactical operators
\newcommand{\ownsoperator}{\mathrel{\textsf{owns}}} % or mathbin
%\newcommand{\ownsoperator}{\mathop{\textsf{owns}}}
\newcommand{\saysoperator}{\mathrel{\textsf{says}}} % or mathbin
\newcommand{\commoperator}{\mathop{\textsf{comm}}}
\newcommand{\createsoperator}{\mathop{\textsf{creates}}}
\newcommand{\tooperator}{\mathrel{\mathsf{to}}}
\newcommand{\defines}{::=}
%\newcommand{\evidence}{\textsf{ev}} % TODO: change font

%% Predicates (are used as pred(...) so are math operators.
%\newcommand{\predicatex}[1]{\mathop{\textsf{#1}}} (use font consistantly mathsf or textsf)
\newcommand{\predicatex}[1]{\mathop{\mathsf{#1}}}
\newcommand{\predicateread}{\predicatex{read}}
\newcommand{\predicatepay}{\predicatex{pay}}
\newcommand{\predicateprint}{\predicatex{print}}
\newcommand{\predicatebelongs}{\predicatex{belongs}}
\newcommand{\predicateemployee}{\predicatex{employee}}
\newcommand{\predicateage}{\predicatex{age}}
\newcommand{\predicatealcoholic}{\predicatex{alc}}
\newcommand{\predicatedrink}{\predicatex{drink}} % serve
\newcommand{\predicaterelated}{\predicatex{rel}}
\newcommand{\predicatepartner}{\predicatex{partner}}
\newcommand{\predicatederived}{\predicatex{derived}} % der

% Authorization/Accountability notions:
\newcommand{\COMAUT}[1]{{\tt ComAut}(#1)}
\newcommand{\OBSAUT}[1]{{\tt ObsAut}(#1)}
\newcommand{\AUTT}[2]{{\tt Aut}_{#1}(#2)}
\newcommand{\AUT}[3]{{\tt Aut}_{#1}(#2,#3)}
%\newcommand{\AUTS}[2]{{\tt AUTS}_{#1}(#2)}
%\newcommand{\ACC}[2]{{\tt Acc}_{#1}(#2)}
\newcommand{\DAC}[1]{{\tt Dac}(#1)}
%\newcommand{\GDAC}[2]{{\tt GDac}_{#1}(#2)}
%\newcommand{\SDAC}[2]{{\tt SDac}_{#1}(#2)}

% constructions
\newcommand{\saysto}[3]{#1 \saysoperator #3 \tooperator #2}
\newcommand{\asaysphitob}{\saysto{a}{b}{\phi}}
\newcommand{\asaysphiotob}{\saysto{a}{b}{\phi_1}}
\newcommand{\ownsad}{a \ownsoperator d}
\newcommand{\createstad}{\createsoperator( t, a, d )}
\newcommand{\createsad}{\createsoperator( a, d )}
\newcommand{\createsidad}{\createsoperator_{id}( a, d )}
\newcommand{\commtabphi}{\commoperator(t, a \Rightarrow b, \phi )}
\newcommand{\commabphi}{\commoperator_{id}( a \Rightarrow b, \phi )}
\newcommand{\readad}{\predicateread(a,d)}
\newcommand{\printad}{\predicateprint(a,d)}

\newcommand{\tvtrue}{\mathsf{true}}
\newcommand{\tvfalse}{\mathsf{false}}

\newcommand{\Ownsad}{A \ownsoperator D}
\newcommand{\Commabphi}{\commoperator( a \Rightarrow b, \phi )}
%\newcommand{\Commabphi}{\commoperator( A \Rightarrow B, \phi )}
\newcommand{\Asaysphitob}{\saysto{A}{B}{\phi}}

%
%% Start text.
%
%\normallatexbib
\begin{document}
%\pagestyle{empty}
%\addtolength{\textwidth}{1cm}
%\addtolength{\textheight}{1cm}

\title{An Audit Logic for Accountability (Extended Version\footnote{This is an extended version of the article to appear in the Conference
Proceedings of the 6th IEEE International Workshop on Policies for
Distributed Systems and Networks (POLICY 2005)} )}
\author{J.G. Cederquist$^1$, R. Corin$^1$, M.A.C. Dekker$^{1,2}$, S. Etalle$^1$ and
J.I. den Hartog$^1$\\[.1in]
$^1$ Department of Computer Science, University of Twente, The Netherlands\\
{\tt \{cederquistj,corin,etalle,hartogji\}@cs.utwente.nl}\\[.1in]
$^2$ Security Department, TNO ICT, The Netherlands\\
{\tt m.a.c.dekker@telecom.tno.nl}\\
}

\maketitle

%\begin{abstract}
%\end{abstract}

%\begin{keywords}
%Privacy, accountability
%\end{keywords}

\centerline{\large \bf Abstract}

\medskip

\noindent
{\it
%Abstract goes here followed by 2 blank lines.
  We describe a policy language and implement its associated proof
  checking system. In our system, agents can distribute data along
  with usage policies in a decentralized architecture.  Our language
  supports the specification of conditions and obligations, and
% associated with the use of the data. We
 also the
  possibility to refine policies.
% e.g.~by adding extra
%  conditions/obligations.
  In our framework, the compliance with usage policies is not actively
  enforced. However, agents are accountable for their actions, and may
  be audited by an authority requiring justifications.

% when
%  audited they have to provide a justification for their actions using
%  the policy logic.
%% To be rewritten.
}

\vspace{2ex}

\section{Introduction}


In many situations, there is a need to share data %information
%(e.g. personal data, music, database records or sensor readings)
between potentially untrusted parties while ensuring the data is used
according to given \emph{policies}.
This problem is addressed by two main research streams:
on one hand, there is a large
body of literature on \emph{access (and usage) control}
\cite{JSSE97,SS94,PS02,BCFP03}, on the other hand we find
\emph{digital rights management} \cite{Wang02,Cho03a}. While the
former assumes a trusted \emph{access control service} restricting
data access, the latter assume trusted devices in charge of content
rendering. Both settings need the trusted components to be available
at the moment the request happens, to regulate the data access.

However, there are scenarios (like the protection of private data) in
which both access control and digital rights management fail, either
because the necessary trusted components are not available or because
they are controlled by agents we do not want to trust.  For instance,
P3P \cite{p3p} and E-P3P (and also EPAL)~\cite{AHKS02} are languages
that allow one to specify policies for privacy protection; however, the
user can only hope that the private data host follows them.

In this paper, the process of regulating the data access is not
assumed to be always performed by the same entity at the same moment
in which the access is requested. More specifically, we relax this in
mainly two ways:
\begin{itemize}
\item
Firstly, at the moment that the data is requested, we assume that
access is always granted, and only later it is determined whether the
requestor had permission to access the data. This is the process of
\emph{auditing}. To achieve this, we need all the relevant decision
information to be kept until audit time (e.g. keeping secure logs).
\item
Secondly, the entity that is performing the auditing does not need
to be fixed, and can thus be dynamically chosen. This is useful
since, for example, some authorities are more appropiate to audit
specific agents than others.  The actual authority does not even
need to be one single entity, and can be for example composed of
regular agents.
\end{itemize}

We present a flexible system which allows to express, deploy and
reason about policies controlling the usage of data. In our target
setting agents can distribute data along with usage policies within
a highly decentralized architecture, in which the enforcement of
policies is difficult (if not impossible). Therefore, we use instead
an \emph{auditing system} with best-effort checking by an authority
which is able to observe (some) actions.  We introduce a notion of
agent \emph{accountability} and express the \emph{proof
  obligation} of an agent being audited.  The system allows to reason
about policies and user accountability. Our framework is depicted in
Figure \ref{fig}.

\begin{figure}
\begin{center}
\input{framework.pstex_t}
\caption{Our framework}
\label{fig}
 \end{center}
\end{figure}

We make no assumptions on the existence of trusted components
regulating access (although we do require a trusted environment to
\emph{certify} environmental conditions, and to securely log
events). In fact, agents are not forced to follow the policies, but
may be audited by authorities which ask for justifications. We make
no particular assumptions about authorities; they may comprise, for
instance, of groups of regular agents. The more an authority can
observe, the more accurate the auditing process is, thus providing
more confidence over the agent's behaviour. To characterize
compliant agent behaviour, as perceived by an authority, we define
\emph{accountability} tests, which are carried out during auditing
by the authority.

Of course, our approach does not allow a strict policy enforcement:
agents can easily ``misbehave'' (i.e. treat data in a way that is not
allowed by the policy), at risk of being traced. It is our
belief that in many emerging scenarios active policy enforcement is
 infeasible.


This paper builds on the preliminary work reported
in~\cite{Cor04b}. In particular, we provide several extensions, the
most notable of which are:
\begin{itemize}
\item
We include the ability to specify conditions and obligations within
the policies.
\item Policies may now contain variables and quantifiers. This allows us to
define a fundamental rule that gives the ability to refine
policies. Agents can create (by refinement) new policies from existing
ones, before passing them to other agents. In contrast, in
\cite{Cor04b} the only policies allowed  are those that are explicitly stated
 by the data owner.
\item We precisely describe our system by introducing
three functions, namely the \emph{observability}, \emph{conclusion
derivation} and \emph{proof obligation} functions.  Moreover, we
provide a customizable action set to account for particular,
user-defined scenarios.
\item We define agent accountability tests, and present a (terminating) procedure for recursive auditing.
\item
Finally, we provide a formalization of our proof system in the proof
checker Twelf\cite{pfenning99system}, which allows us to model
proofs provided by agents, and the subsequent checking by the
authority (Our formalization covers the lower part of Figure
\ref{fig}.)
\end{itemize}

%adding several significantly extensions increasing the expresiveness
%and flexibility of the logic.  [Also: implementation.]
%Deployment.
%%
%%      Ricardo's File
%%

\input{p05-model}

%%
%%      Marnix's File
%%

\input{p05-implement_full}

%% DEBUG: (temporary as implemenation section runs into text)
%\newpage
%{} this space intentionally left blank {}
%\newpage

\input{p05-related}

%%
%%
%%


\section{Conclusions and Future Work}
\label{Conclusions}
\label{FutureWork}
% Tell em what we've done, what others have done and what
% remains to be done.


We have presented a flexible usage policy framework which enables
expressing and reasoning about policies and user accountability.
%Altough being able to specify is also useful in its own right,
%a way to check if pocilies are adheared to greatly increases
%the usefulness/is in most cases needed for deployment of the
%policy framework.
Enforcement of policies is difficult (if not impossible) in the
highly distributed setting we are considering.  Instead, we propose
an auditing system with best-effort checking by an authority depending
on the power of the authority to observe actions.
A notion of agent accountability is introduced
to express the proof obligation of an agent being audited. %...
%A key notion is to use auditing rather than enforcement to create
%a more realistic model.
%enable a flexible system/create a more realistic model.

%This research builds on the work reported in~\cite{Cor04b}.
%The main extentions, compared to , are the addition of variables,
%conditions and obligations, a customizable action set, the ability to
%refine policies and an implementation of our proof system in the
%Twelf proof checker.
%[(more details in following paragraphs)]
%adding several significantly extensions increasing the expresiveness
%and flexibility of the logic.  [Also: implementation.]
%Deployment.

Our obligations cover pre- and post-obligations (\cite{SP03}) but % usage control
not yet ongoing obligations.  The setup does, with an adaption of the
definitions of accountability, seem to provide the means to include
this type of obligations.  Obligations are `use once',
e.g.~$!pay(\$10)$ or `use as often as wanted' $?pay(\$10)$.
%(Counting checked semantically so need for linear logic or similar)
%%One can potentially add a much more complex system here.
%/Future work includes a study of ...
%%We are studing which extensions are useful in expressing policies.
%Case studies/study of examples needed (e.g. chinese wall policies).
% e.g.: adds obligation when communicating relevant data that other party
% does not work on project for competing company and also accepts the
% c.w.p. .

%[more details on refinement?]
%...

%[A paragraph on implementation in Twelf.]
Our proof system has been implemented using the proof checker Twelf.
The agents develop proofs using this implementation. Likewise, the
implementation allows an authority to check the agents' proofs.

%Also
%the notation of proofs used in this framework is suitable for sending
%the proof to an authority which can then (automatically) check the
%provided proof.

%[paragraph on relation with distributed trust management ?]
%Our proof system provides
In our system, we include a % very
 powerful rule which allows
delegating any policy to any other agent.  Agent Alice may
only want to use a policy from Bob if she (i) \emph{knows} Bob, (ii)
\emph{authenticates} Bob, and  (iii) \emph{trusts} Bob.  All these
issues are (intentionally) abstracted away in our approach, as they
seem to be orthogonal to our aims. For example, in (iii), the
required level of trust may depend on the policy provided by Bob or on
the way Alice is going to use the policy.  There, a distributed trust
management system (e.g.~\cite{LMW02}) could be employed to obtain the
required level of trust.
%This issue seems to be
%orthogonal to the creation of policies.

%%One problem we intentionally left unaddressed is that of checking the
%%source of a certain policy. Suppose that $a$ sends to $b$ the policy
%%$\phi$; then the accountability system works properly provided that
%%(i) $a$ is actually the agent he claims to be, and (ii) $a$ will not
%%be able to disappear after the transaction. Making sure that both
%%conditions are satisfied can be done using techniques that are
%%orthogonal to those we presented here.  It is worth remarking that we
%%do not require $b$ to check that $a$ is an authority on $\phi$ (i.e.,
%%that $a$ is actually allowed to transmit $\phi$), this is in fact
%%taken care of a posteriori by the accountability system.

%Our proof system provides a very powerful delegation rule which allows
%delegating any policy to any other agent.  Agent Alice, however, may
%only want to use a policy from Bob if she trust Bob.  The required
%level of trust may depend on the policy provided by Bob or on the way
%Alice is using the policy.  A distributed trust management system,
%e.g.~\cite{?}, could be employed to obtain the required level of
%trust. This issue seems to be orthogonal to the creation of policies.

%% \medskip or intro sentence `future work'.

%further topics of study include fair use, rights revocation,
%integration with trust management.

%%Fair use is a difficult issue in digital rights management, and its
%%definition is still unclear.
%  What is fair use and what is not is
%often not clear and takes extensive study by (human) experts.
%%This
%%makes restricting data access to some policy and while still allowing
%%fair use practically imposible~\cite{Erickson03:ACM}.  Our framework
%%with auditing rather than enforcement allows for modeling of fair use:
%%The system does not need to check the fair use claim but only needs to
%%record it so it can be checked by the authority during an audit.

%Fair use is a difficult issue in digital rights management:
%What is fair use and what is not is often not clear and takes
%extensive study by (human) experts.  This makes restricting
%data access to some policy and while still allowing fair use
%practically imposible~\cite{Erickson03:ACM}.
%Our setting with a posteriory auditing, however, allows a user to
%create new policies which they claim are fair use putting the
%responsibility with the user who knows the exact conditions
%of the use of a policy rather than with the designer of a rights
%management system who has to account for all possibilities.

%One way of modelling fair use in our framework/setup is to simply
%use a policy and claim fair use when audited or, by creating
%a `fair use claim' action which can be used as an obligation for
%deriving the policy.  I.e. using the
%general `law': ${\rm fairuse}(\phi) \rightarrow \phi$ which allows
%use of $\phi$ as long as it is logged as claimed to be fair use.
%Checking the validity of the fair use claims themselfs is done
%by the relevant authority at time of auditing.
%semantical check rather than a syntactical check.
%[One can restrict the fair-use rule to policies $\phi$ which could
%potentially be fair use.]

%Rights revocation, see e.g.~\cite{Sam01}:
In the work of Samarati et.al.~\cite{Sam01}, a
discussion about decentralized administration is presented. Specially,
the revocation of authorizations is addressed. This is a% very
complex problem, which occurs as a consequence of the delegation of
privileges.  One could model revocation of policies by adding a
special flag plus a corresponding check in a policy.
However,
 %\cite{?}  however, assuming that the agent
checking whether a flag is set in another agent's environment is not
realistic in our highly distributed setting.  Further research is needed
to find a both practical and realistic way to include rights
revocation.


Our implementation only covers proof checking. Revisiting
Figure~\ref{fig}, we find that arrows covering policy communications
and logging are not yet implemented. Our framework requires several
properties for each of the different modules (e.g. secure logging and
non-repudiable communications). Certainly, these properties need
cryptography to be realized securely. We regard as future work the
rigorous cryptographic definition of these properties, along with the
accompanying cryptographic constructions.

\paragraph{Acknowledgements}
The research presented in this paper is conducted within the PAW
project (funded by Senter-IOP and TNO), the Inspired Project and the
NWO Account Project.

% Related: `Negative' policies restricting policies and policy refinement.

%Rights revocation, see e.g.~\cite{Sam01}: In \cite{Sam01}, a
%discussion about decentralized administration is made, especially
%about the revocation of authorizations, which is a very complex
%problem, generated by the delegation of privileges.
%This is a very important aspect, and will be also investigated in our
%approach.
% `Negative' policies.
%One can model revocation of policies by added a check of a special
%flag as a condition in the policy.  The problem with this approach,
%however, is that this requires an agent to check a flag which is set
%in the environment of another agent. Assuming that the agent can, at
%will, check a flag set in another agents environment is not realistic
%in our highly distributed setup.
%%Due to the distributed, this is not a trivial matter.
%Further research is needed to find a practical, realistic way of including
%rights revocation.


\old{
%to the framework and the introduction into the setup of an extendable
%action set with corresponding rules in the policy derivation system.
%Furthermore the introduction of variables and universal quantification
%and more general predicates increase the expressive of the logical
%language. % dubbel op.
%enrich the logical language.
%Besides the extended possibilities for specifying allowed and
%disallowed actions, which already has its applications without
%a means of checking/enforcing actions,
%we also provide an implementation schets for our setup and discuss
%requirements for checking different accountability notions.

%However, to extend the usefulness/applicability,
%provide some notes on the implementation of our setup.
% What can still be checked when there are malicious agents.

%more general
%Major extensions:
%- added obligations and conditions, \\
%- introduced more general (and extendable/parameterized) action set
%and corresponding rules in the policy derivation system, \\
%...\\
%minor extensions: variables, more general atomic predicates,...


- Use and extension of the system. (including future work).

We have a flexible extendable setup.
In this section we discuss some notions can be treated/encoded
in our setup and which extensions, if any, are needed.

Our {\bf obligations} cover pre (and post) obligations (\cite{?}) but
not yet ongoing obligations.  The setup does, with an adaption of
the definitions of authorization/accountability, seem to provide
the means to include this type of obligations.
Case studies/study of examples needed (e.g. chinese wall policies).
% e.g.: adds obligation when communicating relevant data that other party
% does not work on project for competing company and also accepts the
% c.w.p. .

As already mentioned\footnote{mention it with definition of agent
accountability.}
obligations are of the type `use once': A single action can only be
used once to fulfill an obligation.  Using a simple tag this can easily
be extended to treat obligations which can be used as often as needed or
used a fixed number of times.\\
- Linear logic\\
- Stronger properties like, after done $x$ once, can do $y$
infinitely often. \\
- Further extentions from simple tags to a full action logic
  e.g. `can use this 10 times action until another action'
  are possible.
We are studing which extensions are really useful in expressing
(privacy) policies.
/Future work includes a study of ...

{\bf Fair use} is a difficult issue in digital rights management:
What is fair use and what is not is often not clear and takes
extensive study by (human) experts.  This makes restricting
data access to some policy and while still allowing fair use
practically imposible.  \cite{Erickson03:ACM}
Our setting with a posteriory auditing, however, allows a
user to create new policies which they claim are fair use putting
the responsibility with the user who knows the exact conditions
of the use of a policy rather than with the designer of a rights
management system who has to account for all possibilities.

One way of modelling fair use in our framework/setup is to simply
use a policy and claim fair use when audited or,
by creating a `fair use claim' action which can be used as an
obligation for deriving the policy.  I.e. using the
general `law': ${\rm fair-use}(\phi) \rightarrow \phi$ which allows
use of $\phi$ as long as it is logged as claimed to be fair use.
Checking the validity of the fair use claims themselfs is done
by the relevant authority at time of auditing.
%semantical check rather than a syntactical check.
% allows restring of fair use to given formats by restricting
% this law.

{\bf Rights revocation}, see e.g.~\cite{Sam01}: In \cite{Sam01}, a
discussion about decentralized administration is made, especially
about the revocation of authorizations, which is a very complex
problem, generated by the delegation of privileges.
%This is a very important aspect, and will be also investigated in our
%approach.
% `Negative' policies.
One can model revocation of policies by added a check of a special
flag as a condition in the policy.  The problem with this approach,
however, is that this requires an agent to check a flag which is set
in the environment of another agent. Assuming that the agent can, at
will, check a flag set in another agents environment is not realistic
in our highly distributed setup. /%Due to the distributed, this is not
a trivial matter. Further research is needed to find a practical,
realistic way of including rights revocation.

{\bf `negative' policies}
related topic: not possible to restrict policies at this time.  Can have
default obligations/conditions for an action, but cannot yet specify this
in a policy. May wish to restrict the owns rule to only allow derivation
of policies of prespecified forms/ Have policies/obligation/requirements
which restrict the building/use of (other) policies.
... Altough we can model restiction e.g. by onging obligation relatively easily
semantically, one want to include it in the derivation system as well.

{\bf Semantics:}
Altough this still needs to be checked in detail, the semantics and
correctness proof for the logic provided in~\cite{Cor04b} seem
to extend to the current extended logic/setting.

%Rights revocation, see e.g.~\cite{Sam01}, and limitations on the right
%to build new policiesare also interesting but difficult points/topics
%which require further study to see if and how they can be added to the
%setup.
%As future work, we plan to address the specification of obligations in
%our policy formula. Another possible path would be to enrich our logic
%by allowing the usage of variables, which would allow us to specify,
%more flexibly, policies that talk about general agents. Our ultimate
%aim is the specification of \emph{Chinese wall} policies.  Another
%interesting issue is the study of right revocation, something already
%discussed in \cite{Sam01}.
%Future work: conditions \& obligations, generalisation for variables in policies, Chinese wall.
%In \cite{Sam01}, a discussion about decentralized administration is
%made, especially about the revocation of authorizations, which is a
%very complex problem, generated by the delegation of privileges. This
%is a very important aspect, and will be also investigated in our
%approach.

[
Move this to conclusions where we can give a more technical description
of the differences: e.g. SAYQ rule, act$\rightarrow\phi$, etc.

...
Continues work reported in~\cite{CELHS:fast04}
In this paper we improve our logic to provide more flexibility, and to
deal with conditions and obligations. We also provide a discussion on
possible deployment/implementation of the system.

\begin{enumerate}
\item We add obligations and conditions.

\item We extend the ability of agents to refine policies, e.g. by
adding extra conditions and obligations to a policy before passing this
to other agents. %(using rule SAYQ).

\item We extend the expressibility of the language by adding:
\begin{itemize}
\item Fully generic atomic predicates, not only relating
  agents and data, but also agents with agents and data with data. We
  show how to encode different data and agents relations.

\item Variables and universal quantifiers to our language. This
  allow us to write much more flexible and powerful policies.
\end{itemize}

\item Finally, we discuss a possible implementation and deployment of
  our system, summarizing the security requirements that need to be
  taken care of.
\end{enumerate}
]
}

%\normallatexbib
%\chapbblname{...}
%\chapbibliography{...}

%\bibliography{project}
%\bibliographystyle{plain}

{ {
\begin{thebibliography}{10}

\bibitem{Aba03}
M.~Abadi.
\newblock Logic in access control.
\newblock In {\em Proc. 8th Annual IEEE Symposium on Logic in Computer Science
  (LICS)}, pages 228--233. IEEE Computer Society Press, 2003.

\bibitem{AF99}
A.~W. Appel and E.~W. Felten.
\newblock Proof-carrying authentication.
\newblock In G.~Tsudik, editor, {\em Proc of the 6th Conference on Computer and
  Communications Security}. ACM Press, 1999.

\bibitem{AHKS02}
P.~Ashley, S.~Hada, G.~Karjoth, and M.~Schunter.
\newblock E-p3p privacy policies and privacy authorization.
\newblock In P.~Samarati, editor, {\em Proc.~of the ACM workshop on Privacy in
  the Electronic Society (WPES 2002)}, pages 103--109. ACM Press, 2002.

\bibitem{BCFP03}
E.~Bertino, B.~Catania, E.~Ferrari, and P.~Perlasca.
\newblock A logical framework for reasoning about access control models.
\newblock {\em ACM Transactions on Information and System Security (TISSEC)},
  pages 71--127, 2003.

\bibitem{Cho03a}
C.~N. Chong, R.~Corin, S.~Etalle, P.~H. Hartel, W.~Jonker, and Y.~W. Law.
\newblock {LicenseScript}: {A} novel digital rights language and its semantics.
\newblock In K.~Ng, C.~Busch, and P.~Nesi, editors, {\em 3rd Int. Conf. on Web
  Delivering of Music ({WEDELMUSIC})}, pages 122--129. IEEE Computer Society
  Press, 2003.

\bibitem{Cor04b}
R.~Corin, S.~Etalle, J.~I. den Hartog, G.~Lenzini, and I.~Staicu.
\newblock {A} logic for auditing accountability in decentralized systems.
\newblock In T.~Dimitrakos and F.~Martinelli, editors, {\em Proc. of the second
  IFIP Workshop on Formal Aspects in Security and Trust ({FAST})}, volume 173,
  page to appear. Springer Verlag, 2004.

\bibitem{DeT02}
John {DeT}reville.
\newblock Binder, a logic-based security language.
\newblock In {\em Proceedings of the {IEEE} Symposium on Research in Security
  and Privacy}, pages 105--113. {IEEE} Computer Society Press, 2002.

\bibitem{JSSE97}
S.~Jajodia, P.~Samarati, V.~S. Subrahmanian, and E.~Bertino.
\newblock A unified framework for enforcing multiple access control policies.
\newblock In J.~Peckham, editor, {\em SIGMOD 1997, Proc. International
  Conference on Management of Data}, pages 474--485. ACM Press, 1997.

\bibitem{LMW02}
N.\ Li, J.\ Mitchell, and W.\ Winsborough.
\newblock Design of a role-based trust-management framework.
\newblock In {\em Proc. of the {IEEE} Symposium on Research in Security and
  Privacy}, pages 114--130. {IEEE} Computer Society Press, 2002.

\bibitem{necula98compiling}
G.~C. Necula.
\newblock {\em Compiling with Proofs}.
\newblock PhD thesis, School of Computer Science, Carnegie Mellon University,
  Pittsburgh, PA, 1998.

\bibitem{PS02}
J.~Park and R.~Sandhu.
\newblock Towards usage control models: Beyond traditional access control.
\newblock In R.~Sandhu, editor, {\em Proc.\ of the Seventh {ACM} Symposium on
  Access Control Models and Technologies ({SACMAT}-02)}, pages 57--64. ACM
  Press, 2002.

\bibitem{pfenning91logic}
F.~Pfenning.
\newblock Logic programming in the {LF} logical framework.
\newblock In G.~Huet and G.~Plotkin, editors, {\em Logical Frameworks}, pages
  149--181. Cambridge University Press, 1991.

\bibitem{pfenning99system}
F.~Pfenning and C.~Sch{\"u}rmann.
\newblock System description: Twelf --- {A} meta-logical framework for
  deductive systems.
\newblock In H.~Ganzinger, editor, {\em Proc. of the 16th International
  Conference on Automated Deduction ({CADE}-16)}, pages 202--206.
  Springer-Verlag, 1999.

\bibitem{Sam01}
P.~Samarati and S.~De~Capitani di~Vimercati.
\newblock Access control: policies, models, and mechanisms.
\newblock In R.~Focardi and R.~Gorrieri, editors, {\em Foundations of Security
  Analysis and Design, LNCS}, volume 2171, pages 137--196. Springer-Verlag,
  2001.

\bibitem{SP03}
R.~Sandhu and J.~Park.
\newblock Usage control: {A} vision for next generation access control.
\newblock In V.~Gorodetsky, L.~J. Popyack, and V.~A. Skormin, editors, {\em
  Proc.\ Second International Workshop on Mathematical Methods, Models, and
  Architectures for Computer Network Security MMM-ACNS}, volume 2776 of {\em
  LNCS}, pages 17--31. Springer-Verlag, 2003.

\bibitem{SS94}
R.~Sandhu and P.~Samarati.
\newblock Access control: Principles and practice.
\newblock {\em IEEE Communications Magazine}, 32(9):40--48, 1994.

\bibitem{p3p}
W3C.
\newblock A p3p preference exchange language 1.0 (appel1.0).
\newblock www.w3.org/TR/P3P-preferences, 2002.

\bibitem{Wang02}
X.~Wang, G.~Lao, T.~{De Martini}, H.~Reddy, M.~Nguyen, and E.~Valenzuela.
\newblock {XrML}: {eXtensible} rights markup language.
\newblock In M.~Kudo, editor, {\em Proc. 2002 {ACM} workshop on {XML} security
  ({XMLSEC}-02)}, pages 71--79. ACM Press, 2002.

\bibitem{WAN04}
N.~Whitehead, M.~Abadi, and G.~C. Necula.
\newblock By reason and authority: A system for authorization of proof-carrying
  code.
\newblock In {\em Proc. of the 17th Computer Security Foundations Workshop},
  pages 236--250. {IEEE} Computer Society Press, 2004.

\end{thebibliography}
}}
\appendix
\input{twelfsugared_cutfree.tex}
\input{audlog_cutfree.elf}



%\bibliography{privacy,project,sandro}
%% %\appendix
%% \section{Soundness Proof}
%% %TODO
%% %\jtodo{Change A\ \  Proofs to Appendix A\ \   Soundness proof.}
%% Before showing our soundness result, we need to introduce the notion of
%% \emph{subproof}.
%% \begin{definition}
%% \label{subp}
%%   Let $\dtree$ be a proof of $\phi$ for $a$ at time $t$
%%   and let $\psi$ be one of the premises of the last rule used in
%%   $\dtree$.  The subtree of $\dtree$ with root $\psi$ is called
%%   a subproof (for $\psi$) of $\dtree$.
%% \end{definition}
%% This is illustrated in Figure~\ref{subprooffig}.
%% \begin{figure}
%%   \centerline{\input{subproof.pstex_t}}
%% \caption{
%% A proof for $\phi$ and its subproof of $\psi$.}
%% \label{subprooffig}
%% \end{figure}
%% We obtain the following intuitive result:
%% \begin{lemma}
%% \label{subproofrem}
%% If $\dtree$ is an authorization proof for $\phi$ at time $t$
%% then any subproof $\dtree'$ for $\psi$ is an authorization proof
%% for $\psi$ at time $t$.
%% % with  $prem(\dtree')\subseteq prem(\dtree)$.
%% %subproof of $\mathcal{P}_\phi$.  If $\mathcal{P}_\phi$ is a
%% %justification for $\phi$ of $x$ at time $t$, then $\mathcal{P}_\psi$
%% %is a justification for $\psi$ of $x$ at time $t$ satisfying
%% %$prem(\mathcal{P}_\psi)\subseteq prem(\mathcal{P}_\phi)$.
%% \end{lemma}
%% This lemma follows from Definition~ \ref{subp} and the fact that
%% premises of a subproof are also premises of the proof.
%% Now we can obtain our soundness result:
%% % TODO: Probleem met implicatie en temporary assumptions.
%% % Opl: normal premise: is also authorization proof, impl or
%% % or premise: logical implication.
%% % if [\phi] --- \psi then \models\phi \rightarrow \models \psi
%% \begin{theorem}[Soundness]
%%   If $\dtree$ is an authorization proof $\phi$ for $a$ at
%%   time~$t$, then $\Evidences\models^t_a \phi$.
%% \end{theorem}
%% \begin{proof}
%%   We proceed by induction on the depth of $\dtree$.  Consider
%%   first the base case, where the proof consists of only one step.
%%   Take cases on $\phi$.
%% \begin{itemize}
%% \item Case $\phi=a \own d$. Then the rule must be a {\tt OWN} rule,
%%   with premise $\creates(t',x,d)$, with $t'<t$.  As $\dtree$ is
%%   an \emph{authorization} proof we have that this premise must
%%   be in $\Evidences$.  By requirement~\ref{creat} of
%%   Definition \ref{semdef}, we obtain the claim.
%% \item Case $\phi=a \say \ \psi \ato b$. Then the rule must be a
%%   {\tt COMM} rule, with premise $\comm(t', a\Rightarrow b, \psi[D])$,
%%   with $t'<t$. Similar to the previous case, we obtain the claim by
%%   requirement~\ref{las} of Definition~\ref{semdef}.
%% \end{itemize}
%% For the inductive case, we take cases on the last step of $\dtree$.
%% %The possible cases are $\wedge{\tt I}$, $\wedge{\tt
%% %  EL}$, $\wedge{\tt ER}$, $\vee{\tt IL}$, $\vee{\tt IR}$, $\vee{\tt
%% %  E}$, ${\tt MP}$, ${\tt COMM}$, ${\tt OWN}$, ${\tt SAY}$, and ${\tt
%% %  DERPOL}$.
%% Consider $\wedge{\tt I}$: We have $\phi=(\psi_1 \wedge \psi_2)$, with
%% premises $\psi_1$ and $\psi_2$. By Lemma \ref{subproofrem}, we have
%% two subproofs $\dtree_1$ for $\psi_1$ and $\dtree_2$ for $\psi_2$ which
%% are authorization proofs. By induction we have that both
%% $\Evidences\models^t_a \psi_1$ and $\Evidences\models^t_a \psi_2$ thus
%% by requirement~\ref{and} of Definition~\ref{semdef} we obtain the claim.
%% The other cases are similar.
%% \end{proof}
\end{document}




%% \author{ R. Corin\inst{1} \and S. Etalle\inst{1,2} \and J. den Hartog\inst{1}
%%   \and G. Lenzini\inst{1} \and I. Staicu\inst{1}}
%
%% \institute{
%%   $^1$Dep. of Computer Science, University of Twente, The Netherlands \\
%%   $^2$ CWI, Center for Mathematics and Computer Science Amsterdam\\
%%   \email{\{corin,etalle,hartogji,lenzinig,staicui\}@cs.utwente.nl} }
%
%% \title{A Logic for Auditing Accountability in Decentralized Systems}
%
%% %\section{Version number: Mon May 17 1:54pm}
%
%\addtolength{\textwidth}{1cm}
%\addtolength{\textheight}{1cm}
%\pagestyle{plain}
%\maketitle

% Access to data / privacy of data.
% who has access to data, can do what with the data/ is allowed
% to do what with the data EP3P.
% What if you do not agree with the policy/ what to place some
% specific restictions on your data...with current approach this
% is not possible.
%  Several approaches to access and usage control exists (see
% the discition in (sub)section~\ref{RelatedWork} )
% Main effort: agent has access or not.  Centrtalized and no
% restrictions are placed on what the agents does with the data
% once its gained access/downloaded it/ ...

\old{
??
\subsubsection{Agent Properties}

The environment can contain whole data and agent relations. This
allows us to express agent properties, and data hierarquies
\cite{}. We provide one simple example:

\begin{example}
  An agent company $c$ has \emph{employee} agents $a_1,...,a_n$.  We
  model this fact by using the atomic predicate
  $\predicateemployee(a_i,c)$, $i\in [1..n]$.  We are interested on
  modelling the situation in which each employee has a database of his
  colleagues.  This can be done by $c$ sending at time $0$ the atoms
  $\predicateemployee(a_j,c)$ to
  each $a_i$, $i,j\in[1..n]$, obtaining:
$$\state_{a_i}(0) = \{\langle comm(b\Rightarrow a_i,
\predicateemployee(a_1,c)), \mathsf{time}(0), \emptyset\rangle, ...,\langle comm(b\Rightarrow a_i,
\predicateemployee(a_n,c)), \mathsf{time}(0), \emptyset\rangle \}$$.

  Also, $c$ can send a policy that allows, for example, any employee
  to read data owned by the company: $\forall
  x,y.(\predicateemployee(x,c) \wedge c \own y) \rightarrow
  (\predicateread(x,y))$ .

  Furthermore , the company may divide their employees by groups, like
  developers, accounting, researchers, etc. We model this by a special
  atomic predicate $\predicatebelongs(b,d)$. Now, the policy that
  associates ownership of data created by an employee to the group she
  belongs: $\forall x,y,z. \predicatebelongs(x,y) \rightarrow (x \own
  z \rightarrow y\own z)$.
\end{example}
}





%&{\tt DERPOL}\ \cfrac{\ a \own d\ }{\phi[d]}{\ a}&
% &{\tt COMM}\ \cfrac{\ \comm(t,a \Rightarrow b, \phi)\ }{a \say \ \phi \ato b}{\ b}&
% \label{1}
% \\
% &{\tt OWN}\ \cfrac{\creates(t,a, d)}{\ a\own d\ }{\ a}&
% \label{2}
% \\
% %&{\tt HAS}\ \cfrac{\creates(i,a, d)}{\ a\ \has\ d\ }{\ a}&\\
% &{\tt SAY}\ \cfrac{\ a \say \ \phi \ato b}{\phi}{\ b}&
% \label{first}
% \\
% &{\tt DERPOL}\ \cfrac{\ a \own
  % d_1\ \ \hdots \ \ a \own d_n}{\phi[\{d_1,\hdots,d_n\}]}{\ a}
% %&{\tt DERPOL}\ \cfrac{\ a \own d\ }{\phi[d]}{\ a}&
%&{\tt DATAPOL}\ \cfrac{\phi(d,b)}{b\ \has\ d}{\ b}&
%&{\tt POL}\ \cfrac{\ a \say \ \phi(d,b) \ato b d\ }{\act}{\ b}
%\label{last}
%\end{eqnarray}

\old{
The first rule (\ref{1}), connects an evidence formula of
``communication'' with a$\say$ policy formula. Intuitively, this
models the fact that if $b$ has evidence of a communication from $a$
of a message $\phi$, then $b$ is allowed to derive the corresponding
$\say$ statement. The next rule (\ref{2}) is analogous for
creation of data. In rule (\ref{first}) we introduce the rule for
the$\say$ constructor, which allows $b$ to ``believe'' something that
$a$ told him. Finally, we have rule (\ref{last}) which states that if
$a$ owns data then she is allowed to derive usage policies for the
data. This rule is indeed crucial in our framework, and also it is
obviously quite powerful.%%  Here,
%Given a formula $\phi$, we assume we can always obtain its \emph{base
%  data} $d$. A formula $\phi$ whose base data is $d$ is
%denoted as $\phi(d)$. In fact,
%%$\phi[D]$ can be thought of as a
%%\emph{usage policy} of $D$.
}

%
%\begin{definition}
%  \label{EvidenceFormulae}
%  The set of \emph{evidence formulae} $\EvidenceFormulae$, ranged over
%  by $\evidence$, is defined by the grammar (with $t\in\Time$
%  $a,b\in\Agents$, $d\in\DataValues$ and $\phi\in\PolicyFormulae_g$):
%  \begin{eqnarray*}
%        \evidence &\defines& \createstad \mid \commtabphi
%  \end{eqnarray*}
%\end{definition}

%In our framework, we include and focus on two ``default'' observable
%actions: data creation and policy communication.  Although we will
%focus on these two actions, we allow other actions to be added as
%extensions to our framework.

\old{
%After creating a data agent~$a$ can conclude that she is the owner
%of this data.
%  To refer to the
%time at which an action has taken place, we define a function
%$\textsf{time}:AC\rightarrow \Time$ as $\textsf{time}(
%\createsoperator(t,a, d) )=\textsf{time}( \comm(t,a\Rightarrow b,
%\phi) ) := t$.
%

% Note that evidence formulas are ground. Indeed, due to our
%  decentralized setting, agent states are completely independent, so
%  shared variables cannot exist.

%\begin{example}
%  The formula $\createsoperator(0,a,d)$ expresses that Alice created
%  data $d$ at time $0$.  The formula $\Scom(1, a \Rightarrow b,
%  \srd(b,d))$ expresses that Alice sent the permission for Bob to read
%  $d$ to Bob at time $1$.
%\end{example}

We have an observability function over actions, $obs: AC \rightarrow
P(\Agents)$. This function maps actions to agents, denoting which
agents may observe an action taking place. For our two basic actions,
we have $obs(\createsad)=\{a\}$ and $obs(\commabphi)=\{a,b\}$.
%We also define
%a function $ag:AC \rightarrow P(\Agents)$, describing the agents
%\emph{taking part} of an action. So, for instance we have $ag(\createsad)=obs(\createsad)=\{a\}$, and $ag(\commabphi)=obs(\commabphi)=\{a,b\}$; However, there may be actions which are observed by agents who do not perform the actions.

Let $D = \{ (agent,action) \ | \ agent\in obs(action)\}$. Then,
actions are linked to our usage policies from the previous section via
two functions, a \emph{conclusion derivation} function $concl:
D
\rightarrow \Phi \cup \{\perp\} $ and a \emph{proof obligation} function $po:  D \rightarrow \Phi \cup \{\perp\}$.

Intuitively, these functions serve, respectively, the purposes:
\begin{itemize}
\item $concl(agent,action)=policy$ states that permission $policy$ may be inferred by $agent$, after observing $action$;
\item $po(agent,action)=policy$ specifies the policy that must be proved by $agent$  to
  validate a performed $action$.
\end{itemize}


 So, for our two actions, we have two related policies (or
 \emph{permissions} derived from observed actions): $concl(a,\createsad)=a
 \own d$, which states that if $a$ created $d$ then $a$ is the owner
 of $d$, and $concl(a,\commabphi)=concl(b,\commabphi)=a \say \
\phi \ato b$, which says that if $a$ sent $\phi$ to $b$ then the corresponding$\say$ policy can be derived by both $a$ and $b$ On the other hand, we have $po(a,\createsad)=\perp$, indicating that $a$ does not need to prove her creation of data. Also, we have $po(b,\commabphi)=\perp$, since data receipt is not required to have permission. However, $a$ is needed to prove her sending data communication: $po(a,\commabphi)=a \say \
\phi \ato b$.

}

%This is illustrated by, for example, Alice sending a policy $\phi$ to
%Bob. Bob can observe the communication, and use the received
%policy. On the other hand, when the authority wishes to ask Alice for
%the permission to perform the communication action, it will enquire
%Alice with the related policy that allows Alice to say $\phi$ to Bob.

\old{
We now present the inference rules that allow us to compose
\emph{proofs}, i.e.~deductions of formulae starting from assumptions
(which in our case are evidences).
In the following inference rules,
we identify:
$$
\llste{NAME}{\mathit{subject}}{\mathit{premises}}{\mathit{conclusions}}
$$
}
%{\tt \wedge I}\ \cfrac{\phi \ \ \ \ \psi\ }{\phi\wedge \psi}{\ a}&{\tt \wedge EL}\ \cfrac{\phi \wedge \psi\ }{\phi}{\ a}&{\tt \wedge ER}\ \cfrac{\phi \wedge \psi\ }{\psi}{\ a}\\
%{\tt \vee IL}\ \cfrac{\phi\ }{\phi\vee \psi}{\ a}&
%{\tt \vee IR}\ \cfrac{\phi\ }{\psi\vee \phi}{\ a}&
%{\tt \vee E}\ \cfrac{\phi \vee \psi \ \overset{[\phi]}{\xi}\ \overset{[\psi]}{\xi}}{\xi}{\ a}\\
%{\tt  MP}\ \cfrac{\phi \rightarrow \psi\ \ \ \ \ \ \phi }{\psi}{\ a}
%&\ \ \ {\tt \rightarrow I}\ \cfrac{\overset{[\psi]}\phi }{\psi\rightarrow \phi}{\ a}&
%

%\subsection{Conditions, Obligations and Environment}

%Conditions are modelled as special \emph{queries} to the
%\emph{environment}, representing the local state of an agent. A query
%to the environment is simply a formula $env(\phi)$ where $\phi$ is an
%atomic predicate.

%Obligations are similar.

%\begin{definition}
%  \noindent
%  \begin{eqnarray*}
%    \phi &\defines&  ... \mid env(p(s_1,...,s_n)) \text{ for }ar(p)=n  \mid obl(p(s_1,...,s_m)) \text{ for }ar(p)=m
%  \end{eqnarray*}
%  \jnote{range over rather than $\in$, can omit}
%  \jnote{or use $\phi\wedge\psi$}
%\end{definition}

\old{

\begin{equation}
\label{proof:eq1}
           \begin{array}{l}
           \llste{\wedge E}{b}
                {[\ageover(x,21) \wedge \alcoholic(y)\wedge
                 \pay(x,m)]}{\ageover(x,21) \wedge \alcoholic(y)}
           \end{array}
\end{equation}

\begin{equation}
\label{proof:eq2}
           \begin{array}{l}
           \llste{\forall E}{b}
                {\forall x,y.  (\ageover(x,21) \wedge \alcoholic(y))
                 \rightarrow \drink(x,y)}
                {\llste{\forall E}{b}{
                         \forall y.  (\ageover(x,21) \wedge
                        \alcoholic(y))\rightarrow \drink(x,y)}
                           {(\ageover(x,21) \wedge
                        \alcoholic(y))\rightarrow \drink(x,y)}%}_{\phi'}}
                }
          \end{array}
\end{equation}

\begin{equation}
\label{proof:eq3}
           \begin{array}{l}
           \llste{MP}{b}
                {\ \ (\ref{proof:eq1}) \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ (\ref{proof:eq2})\ \ }
             {
                 \llste{\rightarrow I}{b}
                {\drink(x,y)}
                { \llste{\forall I}{b}
                        {(\ageover(x,21) \wedge \alcoholic(y)\wedge \pay(x,m))\rightarrow \drink(x,y)}
                        { \llste{\forall I}{b}
                                {\forall x.(\ageover(x,21) \wedge \alcoholic(y)\wedge \pay(x,m))\rightarrow \drink(x,y)}
                                        {\forall x,y.(\ageover(x,21) \wedge \alcoholic(y)\wedge \pay(x,m))\rightarrow \drink(x,y)}
                        }
                }
        }
                        \end{array}
\end{equation}

}



%We improve on this previous work ~\cite{CELHS:fast04}. There, a logic for data
%access and agent accountability was introduced in a setting in which
%data can be created and distributed, along with usage policies.  We
%introduce several notions of accountability; moreover, the logic its
%shown to be sound.

p05-implement_full.tex
\section{Formalization}\label{Implementation}

%In this section we formalize the audit logic.
%In the end of the section, we demonstrate the implementation by formalizing
%example~\ref{sec:proof-system-1}.
%We start with a brief overview of the proof checker Twelf.
%\subsection{Twelf}
%
We have implemented the proof system and checking of the audit logic
in Twelf~\cite{pfenning99system}, which is an implementation of the
Edinburgh Logical Framework~\cite{pfenning91logic}. Research in
proof-carrying code~\cite{necula98compiling} has shown that Logical
Framework (LF) provides a suitable notation for proofs to be sent
and checked by a recipient. In type theories proof checking reduces
to type checking and the LF proof checker is as simple as a
programming language type checker (see also
Section~\ref{RelatedWork}).

%Due to space constraints, the full implementation is not available
%here, although it can be found in the extended version at {\tt
%http://arxiv.org/abs/cs.CR/0502091}.

Here we only mention the most important features of the
implementation. In the appendices we have included both a more
abstract representation (common for a sequent calculus), as well as
the complete Twelf-file.


\paragraph{Audit Logic Implementation}
%To implement the type-checking as proof-checking we need to define
%appropriate types for agents, policies, proof(rule)s, etc.
We first declare the types of the object logic, the atomic
predicates and the actions. Then we present the proof rules and we
finish with an example of a complete proof.
\paragraph{Types}
%In Twelf, a metalogic type is of type \verb@type@. For object logic
%types, we use the type \verb@tp@:
%begin{small}\begin{verbatim}
%  tp: type.
%\end{verbatim}
%\end{small}
%The function arrow \verb@->@, in the meta logic, goes from
% \verb@type@ to \verb@type@ or \verb@kind@ (\verb@type@ has
%type \verb@kind@). Agents, data, actions and policies are declared
%ss \verb@tp@s:
%\begin{small}\begin{verbatim}
%  agent: tp.
%  data: tp.
%  action: tp.
%  policy: tp.
%\end{verbatim}
%\end{small}
%When declaring the rules for the object logic the following type
%constructor is used, which casts arguments from \verb@tp@ to
%\verb@type@:
%\begin{small}\begin{verbatim}
%  tm: tp -> type.
%\end{verbatim}
%\end{small}

In Twelf, a metalogic type is of type \verb@type@. For object logic
types, we use the type \verb@tp@. The meta-logic function  \verb@->@
goes from \verb@type@ to \verb@type@ or \verb@kind@ (\verb@type@ has
type \verb@kind@). Agents, data, actions and policies are declared
as \verb@tp@s. Finally, when declaring the rules for the object logic
the \verb@tm@ type constructor is used,
which casts arguments from \verb@tp@ to
\verb@type@. Summarizing:
\begin{small}
\begin{verbatim}
  tp: type.        agent: tp.    policy: tp.
  tm: tp -> type.  data: tp.     action: tp.
\end{verbatim}
\end{small}
\paragraph{Policies}
Recall that policies are formed with $\ssay$ and $\sown$ and for
example scenario-specific atomic predicates like
$\predicatex{print}$:
\begin{small}\begin{verbatim}
  says: tm agent -> tm policy -> tm agent -> tm policy.
  owns: tm agent -> tm data -> tm policy.
  print: tm agent -> tm data -> tm policy.
\end{verbatim}
\end{small}
For instance, \verb@(print a d)@  is a policy stating that  agent \verb@a@
has permission to print document \verb@d@. Policies can also be
formed using the usual propositional connectives and universal
quantification\footnote{Quantification over policies is not allowed,
so we only instantiate the $\forall$-left and -right rules for the
types agent and data.}(except for negation and disjunction);
to model the different instances of implication in the policy
language (see definition \ref{defPolicyFormulae}), we declare
separate instances for use-once-obligations and
use-many-obligations:
\begin{small}\begin{verbatim}
  imp: tm policy -> tm policy -> tm policy.
  forall: (tm T -> tm policy) -> tm policy.
  and: tm policy -> tm policy -> tm policy.
  ?imp: tm action -> tm policy -> tm policy.
  !imp: tm action -> tm policy -> tm policy.
\end{verbatim}\end{small}
Below we assume that the connectives \verb@imp@, \verb@and@,
\verb@?imp@, \verb@!imp@ are declared as infix-operators.
\paragraph{Actions}
The actions $\scre$ and $\scom$ have the following types:
\begin{small}\begin{verbatim}
  creates: tm agent -> tm data -> tm action.
  comm: tm agent -> tm agent -> tm policy -> tm action.
\end{verbatim}
\end{small}
The \emph{conclusion derivation} function describes the policies the
agent can deduce from some action.
\begin{small}\begin{verbatim}
  concl: tm action -> tm agent -> tm policy -> type.
  concl_comm: concl (comm A B Phi) B (says A Phi B).
  concl_creates: concl (creates A D) A (owns A D).
\end{verbatim}
\end{small}
In Twelf, symbols with a leading capital are variables. Their type
can often be left unspecified, as Twelf expands them to the most
general type.
\paragraph{Proof derivation}
To model local proofs (with respect to agents), we use sequent
calculus formulas of the form $\Gamma;\Delta \vdash_A \Phi$, indicating that
agent $A$ can deduce the policy $\Phi$ from premises $\Gamma$ and
$\Delta$. Here $\Gamma$ is an unrestricted context and $\Delta$ a
linear context. More precisely, $\Gamma$ is a sequent of policies,
actions and ?obligations, while $\Delta$ contains only !obligations.
We formalize this with
\begin{small}\begin{verbatim}
  entail: tm agent -> list nonlin -> list lin -> tm policy -> type.
\end{verbatim}
\end{small}
where \verb@list T@ is the type for lists of type \verb@T@. The type
\verb@nonlin@ is like a disjoint union (policy, action, action) by
the following definitions:
\begin{small}\begin{verbatim}
  nonlin: tp.
  lin: tp.
  act_c: tm action -> tm nonlin.
  ?act_c: tm action -> tm nonlin.
  pol_c: tm policy -> tm nonlin.
  !act_c: tm policy -> tm lin.
\end{verbatim}
\end{small}

\paragraph{Rules}
The rules ${\tt SAY}$ and ${\tt REFINE}$ are defined as follows:
\begin{small}\begin{verbatim}
  say: entail B (cons (pol_c Phi) Gamma) Delta Psi ->
       entail B (cons (pol_c (says A Phi B)) Gamma) Delta Psi.
\end{verbatim}
\end{small}
The $\tt OBS\_ACT$ rule works as follows. If an agent $A$ can
conclude the policy $\Phi$ by observing action {\it act}, then she
can deduce $\Phi$ from any set $\Gamma$ containing {\it act}. In
formula \mbox{$\Gamma,act;\Delta\vdash_A\Phi$}, in Twelf:
\begin{small}\begin{verbatim}
  obs_act:  concl Act A Phi ->
            entail A (cons (act_c Act) Gamma) Delta Phi.
\end{verbatim}
\end{small}
The $\tt REFINE$ rule implements the possibility of \emph{refining}
a policy, $\phi$ to $\psi$ and saying $\psi$, if one has permission
to say $\psi$. Refinement in this sense is expressed using empty
sequents:
\begin{small}\begin{verbatim}
  refine:  entail A (cons (pol_c Phi) nil) nil Psi ->
        entail A (cons (pol_c (says A Phi B)) Gamma) Delta (says A Psi B).
\end{verbatim}
\end{small}
The meaning of the $\tt DER\_POL$ rule is that any formula can be
derived, as long as, for all data affected by it, ownership is
proven. To this end we define a relation on a non-linear sequent
$\Gamma$ and a policy $\phi$, ${\tt op}[\Gamma;\phi]$, that only
holds iff all data affected by $\phi$, occur in some
$\predicatex{owns}$-predicate in $\Gamma$.
\begin{small}
\begin{verbatim}
  op: list nonlin -> tm policy -> type.
  op_imp: (op Gamma Phi) -> (op Gamma (Psi imp Phi)).
  op_forall: ({X: tm data} op Gamma (Phi X)) -> (op Gamma (forall Phi)).
  op_says: (op Gamma Phi) -> (op Gamma (says B Phi C)).
  op_owns: (op (cons (pol_c (owns A D)) Gamma) (owns B D)).
  op_print: (op (cons (pol_c (owns A D)) Gamma) (print B D)).
\end{verbatim}
\end{small}
Now the ${\tt DER\_POL}$ rule is defined as follows:
\begin{small}
\begin{verbatim}
  der_pol: (op Gamma Phi) ->
           entail A Gamma Delta Phi.
\end{verbatim}
\end{small}
Please note that the structural rules and the logical rules for
conjunction, implication and universal quantification over agents
and data are omitted here, but they can be found in the appendices.
\begin{example}[Formalization of Example~\ref{sec:proof-system-1}]
\begin{small}
Recall that Alice creates a document \verb@d@ (a review of a
product) and communicates a policy, to Bob,
 that gives Bob permission to print \verb@d@  'as soon as a related object
 exists'. Below Alice justifies that she can do so. First we declare
 the scenario-specific objects and predicates.
\begin{verbatim}
  a: tm agent. b: tm agent. d: tm data.
  rel: tm data -> tm data -> tm policy.
  phi = forall [x:tm data]((rel d x) imp (print b d)).

  ex2: entail a (cons (act_c (creates a d)) nil) nil (says a phi b)=
        obs_act concl_creates
            (cut
               (der_pol (op_says op_print))
               (refine
                  (forall_r_data [x] (imp_r (w_l init))))
               append_nil2 append_nil).
\end{verbatim}
\end{small}
\end{example}
This theorem has been checked by Twelf. The proof goes along the
same lines as previously in Table~\ref{tabl}.

The lhs can be expressed as $\gamma ;\delta \vdash_a (a\
\predicatex{says}\ \phi\ \predicatex{to}\ b)$, where $\phi$ is
$\forall x.\predicatex{rel}(d,x)\to\predicatex{print(b,d)}$ and
$\gamma$ only contains the creates action, while $\delta$ is empty.
In the proof above, \verb@imp_r@ is the ${\mathit imp}\!{\mathit
-right}$ rule, \verb@forall_r_data@ is the $\forall\!{\mathit
-right}$ rule for quantification over data, \verb@w_l@ and
\verb@init@ are {\it weakening-left} and the {\it initial sequent
axiom} for the non-linear sequent.

p05-model.tex
%
%%      cdeh04-model.tex
%

\newcommand{\Actions}{ACT}
\newcommand{\phiprime}{\phi'}
\newcommand{\Nats}{\mathbb{N}}

\section{A System of Policies and Actions}

Our setup consists of a group of agents executing different actions.
The permission to execute an action is expressed by a policy
constructed using a special logic, introduced below.  In this section
we introduce some necessary components for our system.

\subsection{The basics} % agents, actions and predicates

% two sets, a,d, use capitals if may be variable.
\emph{Agents} are modelled by a set~$\Agents$ ranged over by~$a,b$ and~$c$
(referred to as Alice, Bob, and Charlie).  We also have a
set of agent variables $\Var_a$ and use $A,B,C$ to range over both
agents and agent variables.
Similarly we have a set~$\DataValues$ of \emph{data objects}, ranged over by~$d$,
and a set of data variables $\Var_d$. We use $D$ to range over data objects and
data variables and $x,y,z$ to range over (data and agent) variables.

Basic \emph{permissions} and \emph{facts} are expressed by atomic predicates
in a set $\Predicates$, ranged over by $p$.
Examples are $\readad$, which expresses that agent $a$ has permission
to read data $d$ and $\predicatepartner(a,b)$ indicating (the fact) that
agent $a$ and $b$ are partners.
In general, predicates can relate any number of data objects and agents.
%The arity of a predicate $p$ is denoted by $ar(p)$.

The actions that agents execute are modelled using a set of actions
$\Actions$, ranged over by $act$.  We assume that two types of
actions are always present in this set: Communication (of policies)
$\Commabphi$ and data creation $\createsad$. (Here $a,b$ are agents
and $\phi$ is a ground policy formula, as introduced in the next
subsection).  Our system supports the addition of user-defined
actions.
% Other actions can be added as needed.
\old{
\begin{eqnarray*}
    act &\defines& \createsad \mid \Commabphi \mid \ldots
\end{eqnarray*}
with $\phi$ a ground policy formula (see below).
We will discuss actions in details after introducing the policy language.
[Note on communication, also on creates?]
[Actions model the behavior of an agent, so needs to justify them, but also
 used to fulfill obligations.]
}

\subsection{The Policy Language}

Policies are used to express permissions that agents have, such as the
permission to read a specific piece of data.  Some requirements may
guard a permission. These requirements can be \emph{conditions}, as in
`Alice may read the data if she is a partner of Bob', or
\emph{obligations}, as in `Alice may read the data if she pays Bob
10\$'.  Besides this, a policy may express or relate several different
permissions.  To provide maximum flexibility for writing policies, we
now introduce the following policy language.


\begin{definition}
\label{defPolicyFormulae}
  The set of \emph{policies} $\Phi$, ranged over by $\phi$ and $\psi$,
  is defined by the following grammar:
  \noindent
  \begin{eqnarray*}
    \phi &\defines&  p(s_1,...,s_n) \\&&%\text{ where }ar(p)=n \\&&
                \mid A \own D
                \mid \saysto{A}{B}{\phi}
                \\ &&
                \mid \phi \wedge \phi
%                \mid \phi \vee \phi
                \mid \forall x. \phi
%                \\ &&
                \mid \phi \rightarrow \phi
                \mid \xi \rightarrow \phi
                \\
    s &\defines&  A \mid D \\
    \xi &\defines& !act \mid ?act
  \end{eqnarray*}
\end{definition}
%% Interpretation of the policy formulae:
\noindent First, a policy formula can be a simple predicate
$p(s_1,...,s_n)$, where $s_i$'s can be either an agent, an agent
variable, a data object or a data object variable.  Second, we have
the $\Ownsad$ formula, which indicates that $A$ is the owner of data
object~$D$. As we define below, an data owner is allowed to
create usage policies related to that data.  $\Asaysphitob$ expresses that agent~$A$ is allowed to give
policy~$\phi$ to agent~$B$. The~`$\saysoperator$' policy contains a
target agent to which the statement is said (different from
e.g.~\cite{DeT02,Aba03}).  This allows us to provide a precise way
of communicating policies to certain agents. However, the policy
$\Asaysphitob$ carries a different meaning for source agent $A$ than
target agent $B$: While for agent $A$ it represents the permission
to send $\phi$ to $B$, for $B$ it represents the possibility to use
policy $\phi$ and delegate the responsibility to $A$.

 The logic
constructions \emph{and}, \emph{implication} and
\emph{universal quantification} have their usual meaning.
%[We sometimes abbreviate $\forall x_1...\forall x_n.\phi$ as $\forall x_1,...,x_n.\phi$.]
We actually have two different instances of the implication. The
first, $\phiprime \rightarrow \phi$, has a policy $\phiprime$ as a
\emph{condition}, stating that the agent first needs to establish
this permission or fact before gaining the permission described in
$\phi$. The second, $\xi \rightarrow \phi$, is used to express
obligations. The requirement $\xi$ contains an action that the agent
has to perform when the permission granted by $\phi$ is used.  The
annotations $!$ and $?$ indicate whether the agent needs
to do this action every time it uses $\phi$ or only once. This will
be discussed
in Section \ref{Accountability}.
% intro term `annotated'
%
%We% denote the set of all \emph{ground} formulas,
%i.e. formulas in which each variable $x$ is bound by some $\forall x.$,
%i.e.~formulas without free variables, by $\Phi_g$.
We write $\phi[D]$ to indicate that the set $D$ is the
\emph{data set of $\phi$}, i.e.~all data objects and data variables
occurring in $\phi$.  For instance, we have $\predicateread(b,d)[\{d\}]$.

% can we think up better examples ?
\newcommand{\alcoholic}{\predicatealcoholic}
\newcommand{\ageover}{\predicateage}
\newcommand{\drink}{\predicatedrink}
\newcommand{\pay}{\predicatepay}
\begin{example}
\label{sec:policy-language}
  The (atomic) policy that allows Bob to read the data~$d$ is
  $\predicateread(b,d)$.
  \begin{enumerate}
  \item The policy that allows Bob to read every data object owned by Alice
        is \mbox{$\forall x. (a \ownsoperator x \rightarrow \predicateread(b,x))$}.

      \item Let $\ageover21(x)$ denote that agent~$x$ is at
        least $21$ years old, and $\alcoholic(y)$ denote that
        beverage~$y$
        is alcoholic.  %and $\drink(x,y)$ that $x$ is allowed to drink beverage $y$.
        A policy allowing people over $21$ to drink alcoholic
        beverages is
        $\forall x,y.  (\ageover21(x) \wedge \alcoholic(y))\rightarrow \drink(x,y)$.

  \item If we require a payment of $10\$$  on the previous permission, the policy becomes
  $\forall x.(!paid(x, 10\$) \rightarrow
   \forall y.(\ageover21(x) \wedge \alcoholic(y))\rightarrow \drink(x,y))$.

\end{enumerate}
\end{example}


\subsection{Actions and permissions}\label{actions-and-permissions}

% intro to subsection ...

To distinguish different instances of an action executed in the
system, we label each instance using a unique identifier $id$, as in
$\createsidad$.  This formally gives a set $AC = \Nats \to \Actions$
of `executed actions' or `action instantiations'. However, when
possible, we simply talk about (labeled) actions in $AC$.

Three properties of actions that play a role in our policy system
are described by the following functions:
\begin{itemize}
\item The \emph{observability} function:
  $obs: AC \rightarrow P(\Agents)$
  describes which agents can observe which actions.

\item The \emph{proof obligation} function:
  $po: (AC \times \Agents) \rightarrow \Phi \cup \{\perp\}$
  describes which policy an agent needs to justify the execution of an
  action.  Here $\perp$ indicates that no policy is needed.

\item The \emph{conclusion derivation} function:
  $concl: (ACT\times \Agents) \rightarrow \Phi \cup \{\perp\}$,
  describes what policy can an agent deduce after observing an action.
  Here $\perp$ indicates that no policy can be deduced.

\end{itemize}

While the observability and proof obligation functions depend on
executed actions (i.e.~with identifiers), the conclusion derivation
function is purely syntactical.
% note?


For our default actions $\createsad$ and $\Commabphi$ we have:
\begin{eqnarray}
   obs(\createsad)&=&a
\label{eq:1}
\\
\label{eq:2}
obs(\Commabphi)&=&  \{ a, b \}\\
  po(\createsad, a) &=& \perp
\label{eq:3} \\% &
\label{eq:4}  po(\Commabphi, c) &=& \perp  \quad (a \neq c) \\
\label{eq:5}
  po(\Commabphi, a) &=& \saysto{a}{b}{\phi} \\
  %
\label{eq:6}  concl(\createsad, a) &=& a \own d
\\%  &
\label{eq:7}  concl(\Commabphi, b) &=& \saysto{a}{b}{\phi}
  \\
\label{eq:8}  concl(\createsad, b) &=& \perp \quad (b \neq a)
\\%  &
\label{eq:9}  concl(\Commabphi, c) &=& \perp \quad (c \neq b)
\end{eqnarray}

A creation action by $a$ is observed by $a$ (\ref{eq:1}), while a communication
between $a$ and $b$ is observed by both $a$ and $b$ (\ref{eq:2}).  In other
settings, there may also be other agents that observe
these actions, e.g.~%the ISP of $a$ or
a router standing in between $a$ and $b$.
% might be able to observe the communication between $a$ and $b$.
Agents do not need a policy for creating data (\ref{eq:3}) or receiving a transmission (\ref{eq:4}).
However, sending a transmission \emph{does} require a permission (\ref{eq:5}).
\noindent
%(or at least that there is a communication, not neccessarily its contents).
If agent Alice creates a piece of data she becomes the owner of this data (\ref{eq:6}); any other agent can not deduce the ownership (\ref{eq:8}).
If an agent receives a communication then the agent can conclude the
corresponding $says$ statement (\ref{eq:7}). However, any other agent can not deduce any conclusion (\ref{eq:9}).

\begin{remark}
\label{sec:more-actions}
  Our communication $\Commabphi$ models a point-to-point
  communication. We can easily model broadcasting, by introducing an
  action $\mathsf{bcast}(a,\phi)$, and setting:
  \begin{eqnarray*}
    obs(\mathsf{bcast}(a,\phi)) &=& \Agents  \\
    po(\mathsf{bcast}(a,\phi),x) &=&
        \twocases{
\psi}
{($x=a$)}
                 {\perp}{otherwise}\\
    concl(\mathsf{bcast}(a,\phi),x) &=& \psi%\forall y.a \say \ \phi \ato y
  \end{eqnarray*}
Where $\psi = \forall y.a \say \ \phi \ato y$.

Here, every agent can observe an action $\mathsf{bcast}(a,\phi)$ and conclude that $a$ has broadcasted
  $\phi$ i.e.~said~$\phi$ to everybody. Only $a$ needs to justify this action.
\end{remark}
%A communication from $a$ to $b$ is observed by $a$ and $b$, i.e. we
%set $obs(\commabphi)=\{a,b\}$
%(This models a point-to-point, private
%communication between two parties; other forms of communication can
%also be modelled in our system, see Remark \ref{sec:more-actions} below.)



\subsection{The Proof System}
\label{ProofSystem}

In the previous section we introduced the actions that agents can
execute and the permissions that agents need to justify these actions,
in form of policies.  This section describes how agents perform this
justification, i.e.~how agents can build policies from (simpler) ones.
The possibilities for constructing policies are given in the form of a
\emph{derivation system} or \emph{proof system} for our policy
language.
%We will first present the rules of this derivation system followed by
%a notion of proof.

%Each agent reasons locally about policies, so our inference rules are
%of the form:
%\begin{displaymath}
%  \llste{}{a}{\mbox{premises}}{\mbox{conclusion}}
%\end{displaymath}
Each rule includes, besides the~\emph{premises} and
\emph{conclusion}, an agent $a$, called the \emph{context} of the
proof, indicating which agent is
doing the reasoning.  Our derivation system DER contains the standard
predicate logic rules for introduction and elimination of conjunction,
 implication and universal quantification, together with
the following rules:
%(We omit these for reasons of space.)

\begin{center}
\begin{tabular}{c}
$  \llste {SAY} {a} {b \say \ \phi \ato a} {\phi}$
%  \hspace{2ex}
\\[4ex]%&
  $\llste {REFINE} {a} {\phi \rightarrow \psi \ \ \ \ a \say \ \phi \ato b}
        {a \say \ \psi \ato b}$\\[4ex]
   $\llste {OBS\_ACT} {a}{ act \quad concl(act,a) \neq \perp }
   {concl(act,a)}$
%   $\llste {OBS\_ACT} {a \ \ [a \in obs(act)]}
%        {} {\ \ concl(act)\ \  }$
\\[4ex] %&
%$\llste {ABST\_ACT}{a}{\ \ (?,!)act \ \ \ }{(?,!)act^t}$\\[4ex]
%\\[4ex]
%\end{tabular}\\[4ex]
%\begin{center}
%\begin{tabular}{c}
%$\llste {ENV}{a\ \ [ p(s_1,...,s_n) \text{ ground atom }]}{}{p(s_1,...,s_n)}$  &
 $\llste {DER\_POL} {a} {a \own d_1\ \ \hdots \ \ a \own d_n}
        {\phi[\{d_1,\hdots,d_n\}]}$
\end{tabular}\\[4ex]
\end{center}
%\end{center}
%$$
% SAYSQ => SAYS_MP?, DERPOL -> OWNS?

Rule~(SAY) models delegation of responsibility.  If agent~$b$ says
$\phi$ to $a$ then $a$ can assume~$\phi$ to hold. (It is $b$'s
responsibility to show that it had permission to give $\phi$ to $a$,
see Section \ref{Accountability} on accountability.)  Although agent
$a$ may use $\phi$ without further requirement, it does not mean that
the agent must always do this.  If Bob wants to do a specific
sensitive action, he may only want to use communications that he
`trusts' in building his policy.  For example, Bob would only trust
and thus use a policy `fire Charlie' if it is provided by his boss. If
it is provided to him by coworker Alice, Bob will not use the policy,
even though the responsibility of this policy would rest with Alice.
In this setting, the problem of establishing and managing trust is
orthogonal to the problem of obtaining policies: One could introduce a
trust management system to assign a `level of trust in a proof',
%(the notion of proof is introduced below)
and require that different levels of trust are established for
different actions (see Section 6).

In our logic, Alice can \emph{refine}
her own policies, e.g.~by adding extra conditions and obligations using the standard propositional rules. %extra requirements.
In addition, rule~(REFINE) enables Alice to refine the policies she
provides to other agents: if Alice is allowed to send some policy
$\phi$ then she can also send any refinement of $\phi$. This notion
of refinement isn't easily captured in natural deduction. The
current notation is too general; without further restrictions it
seems that $a$ can derive $\phi\to\psi$ for any (syntactically
unrelated) $\phi$, provided she can assume $\psi$. Thus, we need to
restrict the ability to use assumptions in the subproof of $\phi
\rightarrow \psi$. In the formalization of our model, a double
context sequent calculus, we \emph{can} express this (see Appendix
\ref{sugared}).
%(In other words, this rule gives that $\saysto{a}{b}{\psi}$ refines $\saysto{a}{b}{\phi}$
%when $\psi$ refines $\phi$).
%By using this rule we obtain that if policy $\psi$ {\it refines}
%policy $\phi$ then $\saysto{a}{b}{\psi}$ refines $\saysto{a}{b}{\phi}$.
%An example of the usability of this rule is given in Example \ref{sec:proof-system-1}.
%% i.e. agent can refine its own policies but also the policy he/she provides
%% to somebody else.
%(As a formula: $(\phi\rightarrow\psi) \rightarrow
%(\saysto{a}{\phi}{b}\rightarrow\saysto{a}{\psi}{b})$ for all $\phi,\psi$.)

Rule (OBS\_ACT) links an action with its conclusion, given by
the $concl$ function. (OBS\_ACT)  applies when there
is some conclusion (i.e.~$concl(act,a) \neq \perp$);
%: If Alice observes action $act$ she can draw the conclusion given in $concl(act,a)$.
e.g., from observing action $\Commabphi$ $b$ derives
$\saysto{a}{b}{\phi}$.%, and thus using rule (SAY) $\phi$.
% Note the difference between the policies $\saysto{a}{b}{\phi}$ and $\saysto{b}{a}{\phi}$:
% The first allows Bob to delegate responsibility of $\phi$ to Alice, while
% the second allows Bob to give the policy $\phi$ to Alice.

%Rule (ABST\_ACT) abstracts an action to its action template.
%Rule (ENV) introduces a ground atom provided by the environment.
As we already mentioned, we design the logic in such a way that the
owner of some data $d$ decides who is allowed to do which actions on
$d$. In other words, an owner of some data $d$ is allowed to derive
usage policies for $d$, targeted to any other agent. This is
achieved by rule~(DER\_POL), which allows the creation of any usage
policy for data which the agent owns. Non-owners can refine existing
policies (e.g., policies they received), but cannot create new
policies from scratch.
%This rule is crutial as it allows the creation of usage policies.
%Without this rule agents can refine existing policies, but cannot create
%new policies from scratch.
%%Note that the (DER\_POL) rule is very strong; any usage policy can be created.
%%However, as noted above with the (SAY) rule, additional restrictions may be
%%placed on the actions that can be preformed by other means that the usage policies.
% This is an advantage of the auditing approach over the enforcement approach.
%[Note: very strong rule, may want to restrict. `own(gun) -> shoot(x,gun)'
%but could also check this semantically (similar to trust).
%(crucial as only way to create policies, powerful as can create any policy.)
%]

A derivation with these rules made by an agent is a
\emph{proof}.
% partial proof: allow assumptions: ...

\begin{definition}
  A \emph{proof} $\dtree$ of $\phi$ from agent $a$ is a finite derivation
  tree such that:
  (1) each rule of $\dtree$ has $a$ as subject;
  (2) each rule of $\dtree$ belongs to {\rm DER},
  (3) the root of $\dtree$ is $\phi$, and
  (4) each initial assumption is either an action, an obligation or a basic predicate.
%, and finally
%  (4) each initial rule is either (OBS\_ACT),  (ABST\_ACT), or (ENV).

  We call \emph{conditions} $cond(\dtree)$ of $\dtree$ the initial
  assumptions that are basic predicates, and \emph{actions}
  $act(\dtree)$ the initial assumptions which are observed unguarded
  actions (from rule (OBS\_ACT)). Finally, the multiset of initial
  assumptions that are guarded (by ? and !) actions are called the
  obligations $oblig(\dtree)$ of $\dtree$.  %(The requirements $req(\dtree)$ is the union/combination of these two)
\end{definition}
%`initial assumptions' do not include temporary assumption (which are withdrawn
% after the corresponing implication introduction or or elimination rule.

%[proof of $\phi$ from $\Psi$: as above except leaves may be formulas from $\Psi$.]

We now illustrate the usage of rules (REFINE) and (DER\_POL) in the following example.
% Introduce meaning refinement somewhere

\begin{example}[Policy Refinement]
\label{sec:proof-system-1}
 Suppose we have a predicate $\predicaterelated(d,\bar d)$, expressing whether two
 data objects are related: For instance, $d$ can be a review of a new product
 and $\bar d$ the press release announcing this product.
%Alice owns the review $d_1$ and wants this published as soon as the
%product is anounced. To this end she wants to give a policy to Bob
%that allows Bob to print the document as soon as a related object exists.
%Bob to print the document as soon as a related object exists:
 Alice creates $d$ and wants to give a policy $\forall x.\predicaterelated(d,x)
 \rightarrow \predicateprint(b,d)$ to Bob giving Bob
 permission to print the document as soon as a related object exists:
 % Note that Alice does not own the related data object (it may not even exist (yet)).
 Alice can build the policy allowing her to give this policy to Bob as shown in Table \ref{tabl}.

\begin{table*}
 \begin{equation*}
 \label{proof:eq}
  \llste{REFINE}{a}
  {
    \begin{array}{c}
      \mbox{$[$}\predicateprint(b,d)\mbox{$]$}\\
      \mbox{$[$}\predicaterelated(d,x)\mbox{$]$}\\
      \llste{\rightarrow I}{a}{\predicateprint(b,d)}
      { \llste{\forall I}{a}{\predicaterelated(d,x)\rightarrow\predicateprint(b,d)}
      {        \llste{\rightarrow I}{a}{\forall x.\predicaterelated(d,x)\rightarrow\predicateprint(b,d)}
%                                %{phi}
                            {\predicateprint(b,d)\rightarrow  \forall x.\predicaterelated(d,x)\rightarrow\predicateprint(b,d)}
      }}
    \end{array}
    \raisebox{-3ex}{$
\llste{OBS\_ACT}{a}{
  \begin{array}{c}
  \creates(a,d)\\
concl(\creates(a,d),a))= \ownsad
\end{array}
}{
      \llste{DER\_POL}{a}{\ownsad}
                       {\saysto{a}{b}{\predicateprint(b,d)}}}
    $}
  }
  {\saysto{a}{b}{ \forall x.\predicaterelated(d,x)\rightarrow\predicateprint(b,d)}}
 \end{equation*}
\caption{Proof for Example \ref{sec:proof-system-1}.}
\label{tabl}
\end{table*}

% Alice cannot use the (DER\_POL) rule directly as Alice does not own
% the `data' $x$ which occurs in formula~$\phi$.

 %The tree above is a proof $\dtree$ of ${\saysto{a}{b}{\phi}}$ for $a$ with
 %$cond(\dtree) = \ownsad $, $oblig(\dtree) = ... $
 % Note: not a complete tree, need to establish ownsad for it to be a complete proof.
 % can start with create instead: then starting with an action.
\end{example}

%\begin{example}[Obligations]
%\end{example}



\section{The Model}

%Our setup consists of a group of agents executing actions
%which they justify using policies constructed using a policy logic.
%This section introduces these components while the next section
%describes how the components are combined.

We now introduce a model for our system, combining the different
components of the previous sections.  In our system, agents can
execute and log actions. In addition to agents, an authority is also
present. This authority may audit agents requiring justification for
(some of) the agents actions.

%Below we describe how actions can be logged by agents, followed by the
%formal definition of the system, system state and execution of actions
%in the system. We conclude by defining notions for auditing the
%ccountability of agents.


\old{Finally, we introduce the
authority.  The next section discusses agent accountability which
describes the requirements for agents when audited by the authority.
}


\old{
[change order to\\
- logged act\\
- system \\
- system state \\
- system transitions\\
]
}

\subsection{Logging actions}

Whenever an agent executes an action, it can also choose to
\emph{log} this action.  Logged actions constitute
evidences that can be used to demonstrate that an agent was allowed
to perform a particular action. They are used during accountability
auditing, in Section~\ref{Accountability}.

\begin{definition}
\label{defLoggedAction}
 A \emph{logged action} is a triple
 $lac = \langle act, conds, obligs\rangle$ consisting of an action $act \in AC$, a set of atomic predicates $conds$
 (the `conditions'), and a set of labelled annotated actions $obligs \subset \{!,?\}AC$ (the `obligations').  The set of logged actions is denoted as $LAC$.

\end{definition}

When logging an action, an agent can include supporting conditions
which the environment certifies to be valid at the moment of execution
of the action. This is recorded in the set of predicates $conds$. We do not model the environment explicitly but instead
assume that the agent obtains a secure ``package'' of signed facts
from the environment, represented in $conds$.  As an example, one can
think of the driver's license of Alice being checked to certify that
she is over 21.

An agent can also include obligations in $obligs$ in a logged action,
which refers to other actions the agent did or promises to do.
We abstract away from the details of expressing promises,
and instead assume we have a way to check if actions have \emph{expired}.
%The agent has to perform and log the action before it expires.
%(Expired actions cannot be logged.)
For example, the agent may promise to pay within a day.
Then a payment action needs to be done (and logged) within a day of
logging this obligation. (Also see Section~\ref{Accountability}.)

\begin{example}
We continue with Example \ref{sec:policy-language}.3. Suppose that we introduce an action $\mathsf{drunk}(x,y)$ and a corresponding atomic predicate  $\drink(x,y)$, with
$concl(\mathsf{drunk}(x,y),x)=\perp$ and $po(\mathsf{drunk}(x,y),x)=\drink(x,y)$. We also introduce
 an action $\mathsf{paid}(x,y)$, with corresponding atomic predicate $\pay(x,y)$, with
$concl(\mathsf{paid}(x,y),x)=po(\mathsf{paid}(x,y),x)=\perp$.

A logged action $lac_{\pay}$ for payment is done first by $a$:
 $$
lac_{\pay} = \langle \mathsf{paid}_{0}(a,10\$), \emptyset, \emptyset\rangle
$$

Then, another logged action $lac_{\mathsf{drunk}}$ for the action
$\mathsf{drunk}_{1}(a,beer)$
 is recorded:
\begin{eqnarray*}
lac_{\mathsf{drunk}} &=& \langle \mathsf{drunk}_{1}(a,beer), \\
&&\{\mathsf{age21}(a), \mathsf{alc}(beer) \}, \\
&& \{ !\mathsf{paid}_{0}(a,10\$)\}\rangle
\end{eqnarray*}
\end{example}

The \emph{log of an agent} $a$ is a finite sequence of logged actions.
Note that it does not need to be $a$ who performed the actions, but of course
$a$ has to observe an action to be able to log it.
We say that agent $a$ logs action $act$ when
 $\langle act, conds, obligs \rangle$ is appended
to the log of $a$, where $conds$ is some set of conditions and $obligs$ is some set of obligations.
%That the actions occuring in the log (as logged actions or in the obligations
%of some logged action) must be observable by but not neccessarily executed by $a$

We assume the following consistency properties of logging:
\begin{itemize}
 \item An agent logs any action at most once, thus within
an agent's log the logged actions are uniquely identified by the
label (id) of the action.
 \item An agent can include the same obligation $!act_{id}$ at most once
 within the obligations of logged actions in its log.
 (an $?act_{id}$ action, in contrast, may occur multiple time).
 \item An agent cannot log an expired action.
\end{itemize}

Notice that consistency of the log does not have to be checked at time
of logging, it is sufficient to check it at time of auditing.


%The previous section introduces actions, (ways of building) policies
%in this section the full system model is described.
%%Here we describe how these components are combined into the formal
%%system model.
%We first introduce the system, followed by logged actions and then
%the system state and execution of actions
%

\subsection{The system model and state} % state transitions
We are ready to introduce our system model.
\begin{definition}
\label{system}
A system is a 6-tuple:
\[
\langle \Agents, \Phi, ACT, obs, concl, po\rangle
\] where
$\Agents$ is a set of agents,
$\Phi$ is the policy language,
$ACT$ is a set of actions,
%$I:\Agents \rightarrow P(\Phi)$
%is a mapping from agents to sets of policies, indicating which
%policies hold initially for each agent.  (We denote $I(a)$ as $I_a$.)
and $obs$, $concl$ and $po$ are, respectively, the observability,
conclusion and proof obligation functions.
\end{definition}

%In a system, agents execute by performing actions, some of which are
%observable. Agents can \emph{log} these actions, so that, if later
%they are audited by some authority, they can provide supporting proofs of
%policy compliance.
%We first describe how agents can log actions and then how agents can justify
%their actions when audited.

%\subsection{State and Authority}

A \emph{state} $\state$ is the collection of logs of the different
agents, i.e.~a mapping from agents to logs.
%Given a system as defined in Definition \ref{system} and the notion of
%logged actions as in the previous section, we now define state.  A
%state consists of a mapping from agents to their logs.
%States evolve when agents execute actions.
An agent who observes
an action may choose to log this action.
Thus by executing action $act$ the system can make a \emph{transition} from
a state $\state$ to state $\state'$, denoted $\state\overset{act}{\rightarrow}\state'$
where $\state'$ equals $\state$ except that the action $act$ may have
have been logged by any agent $a$ that can observe the action, $a\in obs(act)$.
% Logging action $act$ of $a$ in state $\state$ is updating $\state(a)$ by
% appending a logged action $act$ is any logged
%Formally:
%$\state'(a) = \state(a)$ if $a\notin obs(act)$ and
%$\state'(a) = \state(a) . optional\_log\_of(act)$ if $a\in obs(act)$
%assumption, though, we require that agents can only log an action at the
%same moment in which the agent executes it, and not at a different
%moment.
An \emph{execution} of the system consists of a sequence of transitions
$\state_0 \overset{act_1}{\rightarrow} \state_1 \overset{act_2}{\rightarrow}... \overset{act_n}{\rightarrow}\state_n$,
starting with some initial state $\state_0$. %=\emptyset$ ?]
The \emph{execution trace} for this execution is $act_1\,act_2...\,act_n$.
Actions logged by an agent can be also seen as a trace of
actions, by projecting only the actions of each logged action. We
denote that trace as $\state(a)$. Let $\preceq$ denote the subtrace
relation ($tr_1 \preceq tr_2$ if each action of $tr_1$ is included in
$tr_2$, and each time an action $act_1$ appears before $act_2$ in
$tr_1$, the $act_1$ also appears before $act_2$ in $tr_2$). We have
$\state(a)\preceq tr$.


\old{ Initially, we have the state $\state_0 =
  \emptyset$. To denote a transition, we use a labelled
  $\overset{act}{\rightarrow}$.  So, for example, we have that
  $\state_0 \overset{act}{\rightarrow} \state_1$, for $act \in AC$. If
  $act = \commabphi$, then we can have $\state_1 = \{a \rightarrow
  logact\}$, in which $a$ logs the communication (but not $b$). We
  denote $a$'s log in a state $\state$ as $\state^a$.  Given a series
  of transitions $\state_0 \overset{act_0}{\rightarrow} \state_1
  \overset{act_1}{\rightarrow}... \overset{act_i}{\rightarrow}
  \state$, we denote the sequence of actions $act_0,act_1...,act_i$ as
  an \emph{execution trace} $tr$.

 Note that we agents may log actions, but this is not a requirement.
not logging actions, however, can, in some cases, make it difficult for
the agent to show policy compliance.
}

%\subsection{The Authority}
\paragraph{Auditing Authority}
Agents may be audited by some \emph{authority}, at some
state $\state$.  Intuitively, when some agent is about to be audited,
an auditing authority is formed. This authority will audit
the agent to find whether she is accountable for her actions.
% (this
%process is made more precise in the next section).
%
%%First, the authority will inspect the log of the agent $a$ being audited
%%by validating each logged action in $\state(a)$.
%
% Different strengths of the authority: how much of the system can
% it see, how many other agents cooperate with the authority, etc.
% all this expressed in given the evidence set.
%%However, the authority may also require the agent to justify actions
%%\emph{not} in $\state(a)$, but still observed in the system. More
%%precisely,
Let $tr$ be the sequence of actions executed from some initial state
to $\state$,
The
\emph{evidence} trace, denoted $\Evidences$, contains all the actions that might be
audited. Initially, $\Evidences$ embeds
$\state(a)$. However, $\Evidences$ may also contain actions not in
$\state(a)$: They may be provided, for example, by some observing
agents. However, we assume that given $\state(a)$ and other observed
actions $S$, the authority can order properly the actions of
$\state(a)$ and $S$ into $\Evidences$, s.t. $\Evidences \preceq tr$.
Thus, in general $\Evidences$
 is a
trace satisfying $\state(a) \preceq \Evidences \preceq tr$.

%The closer $\Evidences$ is to its upper bound, the more it can audit from $a$.





% -> subsection (also adjust references to `Section Accountability')
\subsection{Accountability}
\label{Accountability}

We now introduce notions of agent accountability, determined by some
authority in possession of evidences. These definitions allow an
authority to audit agents, to establish whether the agent was allowed
to do the actions he did. In previous work \cite{Cor04b}, we defined
several notions of agent and data accountability, but without checking
for obligations nor conditions. We did not have logs of agents
either. We now define accountability for logged actions, which we then
extend to agent logs.


We first introduce \emph{justification} proofs for logged actions.
Intuitively, a justification proof is a proof of the policy required
for the action (as given by function $po$), using only conditions and
obligations that have been logged.

\begin{definition}
  A proof $\dtree$ of $\phi$ from $a$ is a justification (proof) of logged
  action $\langle act, conds, obligs\rangle$ if:
  \begin{itemize}
    \item $po( act, a ) = \phi$
    \item The obligation in the proof are included in $obligs$;
        %$oblig(\dtree)\subseteq obligs$ (if an action $!act$ occurs $n$ times in
        %$oblig(\dtree)$ then there are $n$ different ids with $!act_{id}$ in $obligs$.
        `$oblig(\dtree) \subset obligs$'.
        (Here multiple $?act$ in $oblig(\dtree)$ may be assigned to the same $?act_{id}$ but
         each occurrence of $!act$ must have its own $!act_{id}$ in $obligs$.)
        \footnote{interpreting as sets for $?act$ and as multisets for $!act$.}
        %such that each $?act'$, $!act'$ is mapped to some $act'_{id}\in obligs$ and
        %no two $!act'$ map to the same action $act'_{id}$.
    \item Each condition in the proof is in $conds$;  $cond(\dtree) \subseteq conds$.
  \end{itemize}

  The set of all justifications is denoted by $\mathcal{J}$.
\end{definition}

%[note on the obligations:
% %obligs(\dtree) is a multiset of (unlabeled) actions, while obligs is a set of labeled actions.
% The proof system uses unlabeled (annotated) actions, and the actions in the log are labeled with an id.
% We mostly ignore the id label of actions but here we need to be precise to prevent
% e.g.~a single pay action being used to fullfil two different payment obligations.]

In general, there may be different justifications for an action.  The
justifications provided by the agent are modeled by a function ${\tt
  Pr}: \Agents \times LAC \rightarrow \mathcal{J}\cup\{\bot\}$.  Here
${\tt Pr}(a,\langle act, conds, obligs\rangle)$ is either a valid
justification of $\langle act, conds, obligs\rangle$, or it is $\bot$,
indicating that the agent did not provide a justification.

%\subsection{Agent Accountability}
%We are ready to define accountability for a logged action:

%A logged action $logact = \langle act, conds, obligs\rangle$ is valid, denoted $LAA(\state^a,logact)$, if
\begin{definition}[Logged Action Accountability]
\label{sec:accountability}
   Agent $a$ correctly accounts for logged action
  $logact = \langle act, conds, obligs\rangle$ (in state $\state$), denoted $LAA(a,logact)$, if:
  \begin{itemize}
  \item if $po(act,a) \neq \bot$ then ${\tt Pr}(a,logact)\neq \bot$, i.e.~if needed a justification is provided
  \item if $o\in obligs$ has expired then $o\in\state(a)$, i.e.~each obligation that has expired has been
        (executed and) logged.
\item For each $act \in act({\tt Pr}(a,logact))$, $a$ provides an $id$
s.t. $act_{id}$ occurs in $tr$ and $a\in obs(act_{id})$\footnote{We assume the authority can verify this.}


  \end{itemize}
\end{definition}%
This definition introduces accountability for a single (logged) action. We now
define accountability for any action and for
all audited actions.
%{\bf What happened to the checking of ? and ! for all proofs?}

% Recall that the authority requires justification for a set $\Evidences$
%of actions.]

\begin{definition}[Action Accountability]
\label{sec:accountability-1}
We say that agent $a$ correctly accounts for (labeled) action $act$, denoted $AA(a,act)$, if
  \begin{itemize}
   \item $a$ has logged $act$ as $logact$ and $LAA(a,logact)$ or
   \item $a$ has not logged $act$ and $LAA(a,\langle act, \emptyset, \emptyset \rangle)$
  \end{itemize}

  We say agent $a$ passes audit $\Evidences$, written
  $ACC(a,\Evidences)$, if either $\Evidences$ is the empty trace, or
  $\Evidences = \Evidences'.act$ with:
\begin{itemize}
\item $AA(a,act)$
\item $ACC(a,\Evidences'')$, with $\Evidences''$ the correct ordered
  merge of $\Evidences'$ and $newacts$, all the \emph{new}
  actions (i.e. not already in $\Evidences'$) given by the proofs in $AA(a,act)$.
\end{itemize}
%Finally, for $ACC(a,\Evidences)$ to
%  hold, all provided proofs are checked for consistency of usage of
%  banged ($!$) actions.
%$a$ correctly accounts for all actions
%  in $\Evidences$.
\end{definition}%

%
%\begin{definition}
% We write $ACC(a)$ if:
% \begin{itemize}
%   \item $\forall logact \in \state(a) : LAA(a,logact)$; and
%   \item $\forall act\in \Evidences$ not logged by $a$: $LAA(a,\langle act, \emptyset, \emptyset \rangle)$
% \end{itemize}
%\end{definition}

%Thus for actions the agents has not logged must be justificated without
%the use of conditions and obligations;

The second case for action accountability explains why it can be in
the interest of an agent to log its actions.  As conditions may
have changed, the agent can only rely on conditions if they have
been logged at the time the action was executed. For
example, if some action had a condition `only execute between 4 p.m.
and 4:30 p.m. on 12/10/2004', then that condition would only hold
temporarily; If an agent executed the action and did not log it,
during a later audit the agent could not provide a valid proof. The
same holds for obligations: Only obligations logged with the action
can be used in a proof of the action.

\begin{claim}
\label{sec:accountability-3}
Let $a$ be an agent and $\Evidences$ an evidence trace. Then, checking $ACC(a,\Evidences)$ terminates.
\end{claim}
\emph{Proof.} Let $|tr|=n$, for some $n\geq 0$.  Suppose
$|\Evidences|=m\leq n$.  We show that each execution of $ACC(a,\Evidences)$ decreases $l$, with $l = n$ initially.
After every execution of
$ACC(a,\Evidences)$ as in Definition~\ref{sec:accountability-1}, at
most $l-m$ evidences (the $newacts$) are added to $\Evidences''$.
Thus, $|\Evidences''| = |\Evidences'| + (l-m) = m-1 + (l-m) = l-1$. Hence, $ACC(a,\Evidences)$ terminates.

%The possibility of adding (fullfilled) conditions and obligation explains why
%it can be in the interest of the agent to log an action.
%To prove authorization
%to do the action, the agent may need to rely on these conditions and obligations.
%- Related with definition of accountability, or move there.


%authorized to execute all her observed actions (up to the authority's
%view), i.e.~$\forall
%act \in \Evidences:  \AUT{po(a,act)}{a}{T}$.
%  \jtodo{add $t\leq T$ or note that any evidence with $t>T$ cannot be in evidence
%   set used when auditing ?}
%    Finally, we say that agent $a$ passes the \emph{accountability} test,
%  written $\ACC{}{a}$, if both $\AUTT{}{a}$ and $\OBSAUT{a}$ hold.
% $\forall \comm(t,a \Rightarrow b, \psi) \in \SEvids:\AUTT{}{{\tt Pr}(a \say \ \psi \ato b),a,t}$
%\end{itemize}

\paragraph{Honest Strategy}

A strategy for an honest agent $a$ to always be accountable is as
follows.  Before executing some action $act$, $a$ checks whether
$po(act,a)$ is derivable. If any obligation needs to be fulfilled,
then the agent performs and then logs it. If any condition or
obligation needs to be fulfilled, then the action $act$ is also
logged. Then, it follows from the definitions that:
\begin{remark}[Accountability of honest agents]
  If agent $a$ follows the \emph{honest strategy}, then for any
  system execution and any auditing authority with evidence set $\Evidences$,
  we have that $ACC(a,\Evidences)$ holds.
\end{remark}
The proof follows immediately from Definitions
\ref{sec:accountability} and \ref{sec:accountability-1}.

\paragraph{Recursive auditing}

We have, up to now, defined accountability of one particular agent in
isolation. However, we may be interested in cross-verifying the
actions of agents.
% that is, to audit one \emph{suspected} agent and,
%from the agent's justification proofs, obtain new \emph{suspects} and
%new evidence actions, which in turn need to be audited.
%
We sketch an algorithm for recursive auditing of agents, which can be
used by a potential auditing authority. The algorithm inputs $S_0$, a
set of \emph{suspected} agents, and $\Evidences_0$, an initial
evidence trace. Given $ACC(a,\Evidences)$, we write
$E(ACC(a,\Evidences))$ to denote the set of new actions appearing in
the given proofs (the $newacts$ in Definition
\ref{sec:accountability-1}), and $A(ACC(a,\Evidences))$ the
corresponding set of agents appearing in these actions for which the
proof obligation is not bottom, i.e.~$po(\cdot,\cdot)\neq \perp$.

\begin{algorithm}[Recursive Auditing]
\label{sec:trac-agents-algor}
Inputs: $S_0$ and $\Evidences_0$. Outputs: {\bf true} if audited agents are accountable, {\bf false} otherwise. \\[2mm]
{\small
\begin{tabular}{l}
1. $S$:=$S_0${\tt ;}\\
2. $\Evidences$ {\tt :=} $\Evidences_0${\tt ;}\\
3. {\bf while }$S$ $\neq \emptyset$ {\bf do}\\
4. \ \ {\bf let }$a \in S${\tt ;}\\
5. \ \ {\bf if }$ACC(a, \Evidences)$\ {\bf then }\\
6. \ \ \ $S${\tt :=}$(S \setminus \{a\}) \cup  A(ACC(a,\Evidences))$\\
7. \ \ \ $\Evidences$ {\tt :=} $\Evidences \cup E(ACC(a,\Evidences))$\\
8. \ \ {\bf else }\\
9. \ \ \ {\tt return} {\bf false}\\
10. {\bf end }\\
11. {\tt return }{\bf true}
\end{tabular}
}
\end{algorithm}

\begin{claim}Algorithm \ref{sec:trac-agents-algor} terminates.
\end{claim}
\emph{Proof.} Similar to the proof of Claim \ref{sec:accountability-3}.

\begin{claim}In line 4 of of Algorithm \ref{sec:trac-agents-algor}, the order in which the agents are chosen does not matter.
\end{claim}
\emph{Proof (sketch).} Follows from the fact that proofs are fixed on
beforehand, as given by function ${\tt Pr}: \Agents \times LAC
\rightarrow \mathcal{J}\cup\{\bot\}$, and do not depend on knowing
whether other agents are being audited or not. (Intuitively, this
models the fact that agents can not change their proofs on the fly,
depending on whether other agents are being audited.)

p05-related.tex
\section{Related  Work} \label{RelatedWork}

%\renewcommand{\cite}[1]{[#1]}
%DEBUG: show link name rather than doing actual reference
%for easy proof reading.

%describe binder
There is a wide body of literature on logics in Access Control (see
the survey by Abadi~\cite{Aba03}). Here, we mention some of the
proposals. Binder~\cite{DeT02} is a logic-based security language
%designed by John DeTreville, and
% To suit a
%distributed deployment,
%Binder is monotonic and it also allows for authorization proofs to be
%generated remotely, while only verified by the access-point.
%
%Binder
%it is
 based on Datalog
%(Prolog without function symbols).
%and is a first-order predicate logic.  This means that queries in the
%policies are decidable in polynomial time.
 Binder includes a special predicate, \textit{says},
 used to quote other agents.  Binder's \emph{says} differs in two
 aspects from our construct: First, ours
 includes a target agent (see Section~\ref{ProofSystem}); Second, when
 importing (i.e.  communicating a policy in our setting) a clause in
 Binder, care must be taken to avoid nested \emph{says}, since it may
 introduce difficulties in their setting.
%
%, which if allowed in their
%setting it might introduce difficulties.
%
%
%
%A quoted statement remains
%inert, unless trusted explicitly by the importing Binder context. For
%instance, "trust B on saying who is good" in Binder reads: good(X) :-
%B says good(X). On the contrary, the delegation of responsibility
%modelled in Audit Logic allows for any quote from anyone to be used in
%a proof (see also \ref{section3} on this).
%
%The impossibility to nest
%says in says, complicates importing rules.  For instance when A
%exports the above rule, one gets A says good(X) :- B says good(X).
%Therefore Abadi proposes the axiom (B says S) -> (A says B says S) to
%achieve this\cite{Aba03}. The validity of a Binder proof varies in
%time, for example when deploying short-lived statements a proof
%expires after generation.  Something which in our auditing framework
%never happens.  Finally, actions and state, for instance to model
%'play movie 2 times' can not be expressed in Binder.
%
%describe appel
More related to our auditing by means of proofs, Appel and Felten~\cite{AF99}
propose the Proof-Carrying Authentication framework (PCA),
also implemented in Twelf (see
Section~\ref{Implementation}).
% and in the paper the size of some sample proofs is
%analyzed.
Differently from our work, PCA's language is based on a higher order
logic that allows quantification over predicates. Also, their system
is implemented as an access control system for web servers, while in
our case we focus on a-posteriori auditing.
%Now there is no
%general algorithm to make decisions on higher order rules but in PCA
%the proof-burden is put on the requester. An advantage of
%quantification is that the server can use one basic logic, to decide
%on any application-specific predicates (which are proven as lemma's by
%the requester). The system is implemented as an access control system
%for webservers.
%%Moreover, the \emph{says} predicate is also treated differently than
%%ours (they use the axiom: $P\ \rightarrow\ A\  says\  P$ to express that
%%propositional tautologies are said by all principals).
%In addition to
%this Appel and Felten propose deployment of the controls predicate
%with the axiom: $A controls P, A says P -> P$, to grasp the idea of
%believing agents on certain statements, but not on others. Again says
%is treated quite differently in Audit Logic (see \ref{section3}.

BLF~\cite{WAN04} is an implementation of a Proof-Carrying-Code framework that uses
both Binder and Twelf, which however focuses on checking semantic code
properties of programs.

%refer to abadi's survey and work
%A good overview of logics in access control can be found in a
%survey by Abadi\cite{Aba03} and for a detailed treatment of
%concepts like channels, keys, roles, quoting and speaksfor we
%refer to the paper 'A Calculus in Access Control' by Abadi et
%al.\cite{ABLP93}.
%refer to more distant systems RT, DL, Blaze

%Not so close to ours, but addressing similar problems are several
%certificate systems (like KeyNote~\cite{Bla99} and SPKI/SDSI~\cite{HM99}) have
%been proposed that deal with distributed authorization or Distributed
%Trust Management. However these systems fail to handle certain common
%forms of delegation. Much more suitable for
%delegation is Li~et~al.'s RT-framework~\cite{LMW02}, which combines role-based
%access control and trust management systems.

%more general to get to Sandhu & Samarati, Bertino and EP3P
Sandhu and Samarati~\cite{SS94} give an account of access control
models and their applications. Bertino et al.~\cite{BCFP03} propose
a framework for reasoning on access control models, in which
authorization rules treat the core components Subjects, Objects and
Privileges. Sandhu and Park~\cite{PS02} take a different approach
with their UCON-model, in which the decision is modelled as a
reference monitor that checks the 3 components: ACL, Conditions and
Obligations. This reflects much the separation also made by us.
Obligations and conditions are also prominent in directives on
privacy and terms of use in DRM. The concept of \emph{purpose} of an
action is not used by us, but is used in the privacy languages P3P
and E-P3P~\cite{AHKS02}.  Unlike our policy language, E-P3P allows
the use of negation, which requires special care to avoid problems
in a distributed setting.

twelfsugared_cutfree.tex
%\documentclass[12pt]{article}
%\input{preamble_p05}

\newcommand{\ALFA}{\small ALFA\ }
\newcommand{\action}[1]{#1}%_{act}}
\newcommand{\condition}[1]{\predicatex{#1}}%_{cnd}}
\newcommand{\slt}[1]{\small{#1}}
\newcommand{\entailm}[4]{\ \ {#2};{#3} \vdash_{#1} #4\ \ }
\newcommand{\entail}[3]{\ \ { #2} \vdash_{#1}#3\ \ }
\newcommand{\seqinf}[3]{\scriptstyle{\tt #1 }\genfrac{}{}{.8pt}{0}{#2}{#3}}
\newcommand{\seqinflarge}[3]{\tt #1 \cfrac{ #2}{ #3}}
\newcommand{\treeinf}[3]{\scriptstyle{\tt #1 }\genfrac{}{}{.8pt}{0}{#2}{#3}}
\newcommand{\vdinf}[1]{\genfrac{}{}{0pt}{0}{\text{\ }}{#1}}
\newcommand{\limp}{\tt{\ ! imp\ }}
\newcommand{\mimp}{\tt{\ ? imp\ }}
\newcommand{\pred}[1]{\mathop{\mathsf{#1}}}
\newcommand{\ADTS}[2]{{\tt op}[#1;#2]}

%\begin{document}
%\title{Sugared Twelf\\\small{Sequent calculus for the Audit Logic}}
%\maketitle
\section{The Sequent calculus for the Audit Logic}
\label{sugared}
In Twelf we implemented a double context sequent
calculus. To explain the Twelf-code more clearly, we start by giving
the (for sequent calculi) common representation of our system. In
the formalization of our model we have in general
$\entailm{A}{\langle \text{context}\rangle}{\langle \text{linear
context}\rangle}{\text{policy}}$, \textbf{where $A$ is the agent
doing the reasoning, but below we can write shortly} $\entailm{\
}{\Gamma}{\Delta}{\phi}$ (because rules regard only one
agent-context). The contexts are sequents of linear and nonlinear
propositions that serve as premises for the conclusion (right of the
$\vdash$ sign). Now, in the Twelf code we declare 6 types of
objects: agent, data, action, policy, nonlin, lin and a type list.
In the sequel Greek and Roman letters denote variables that range
over them. The type of the variables is often left implicit, so to
distinguish the different types we use; $\tt{A,\ B,\ C}$ to denote
agents, $\tt{\Gamma,\ \Gamma '}$ for lists of type nonlin,
$\tt{\Delta,\ \Delta'}$ for lists of type lin, $\gamma_0$ and
$\delta_0$ for the empty lists of type lin and nonlin. Policies are
denoted with $\tt{\phi,\ \phi',\ \psi}$ and $\tt{\xi,\ \xi'}$ denote
actions. To express append and construct operators for lists we just
write a comma. And finally $\to, \wedge, \forall$ denote the policy
connectives for implication, conjunction and universal
quantification. We use $\mimp$ and $\limp$ for the implication
operators on obligations. Finally, in the non-linear context, we mix
policy formulas (introduced by the standard logical rules), with
actions (introduced by obs\_act) and use-many-obligations
(introduced with $\mimp$). In Twelf each of these is mapped to the
type nonlin. This context is thus like a list of the disjoint union
of policy, action and action.

Below we only mention the main inference rules. For the type
declarations and the definitions of lists and so on we refer to the
Twelf code in the appendix.

First our pivotal rules. Here we mention the $A$ in $\vdash_A$
because the agent appears explicitly in the formulas.
\begin{eqnarray*}
&&\seqinflarge{SAY}{\entailm{A}{\Gamma,\phi}{\Delta}{\psi}}
{\entailm{A}{\Gamma,\pred{says}(B,\phi,A)}{\Delta}{\psi}}
\\\\
&&\seqinflarge{OBS\_ACT}{\entailm{\
}{\Gamma,\emph{concl}(\xi,A)}{\Delta}{\psi}}{\entailm{A}{\Gamma,
\xi}{\Delta}{\psi}}
\\\\
&&\seqinflarge{REFINE}{\entailm{A}{\gamma_0,\phi}{\delta_0}{\psi}}
{\entailm{A}{\Gamma,\pred{says}(A, \phi,B)}{\Delta}{\pred{says}(A,
\psi,B)}}
\\\\
&&\seqinflarge{DER\_POL}{\ADTS{\Gamma}{\psi}}
{\entailm{A}{\Gamma}{\Delta}{\psi}}
\end{eqnarray*}
Note the apparent difference with for instance the {\tt SAY}-rule in
natural deduction style in Section \ref{ProofSystem}. It seems to
have been turned upside-down; this is done to both keep the
sub-formula-property, and preserve the redundancy of the
cut-rule\footnote{A full proof of cut-admissibility and other
meta-theorems are future work}.

The {\tt OBS\_ACT}-rule uses the conclusion derivation function,
which is defined as:
\begin{eqnarray*}
            &&{\tt concl\_creates}:\ concl(\action{creates}(A,D), A) = \text{\tt owns}(A, D).\\
            &&{\tt concl\_comm}:\ concl(\action{comm}(A,B,\phi),B) = \text{\tt says}(A,\phi,B).
    \end{eqnarray*}

A few words on the {\tt REFINE}-rule: The intention of the empty
sequents is to prevent that an agent uses a fact $\psi$ to derive
$\phi\to\psi$ for an otherwise unrelated $\phi$. In formulas:
$\Gamma,\psi\vdash(\phi\to\psi)$ holds for any $\Gamma$ and $\phi$.
Then with just the permission to \emph{say} $\phi$, the agent can
\emph{say} $\psi$, which is of course not the meaning of
\emph{refining} the policy $\phi$. This subtlety is not easily
expressed in natural deduction rules, but in the sequent calculus
this is done straightforwardly with the empty sequent $\gamma_0$.
With this restriction in place only syntactically related policies
can be used, for example for $\psi=(\xi\to\phi)$ or
$\psi=\forall\phi$. While, if there exists such a relation for two
(syntactically unrelated) predicates, then it should be expressed by
adding a rule for it:
$\gamma_0,\pred{write}(A,D)\vdash\pred{read}(A,D)$.

Finally, the {\tt DER\_POL}-rule expresses that if a policy sets
permissions on data $D_1,...,D_n$ and each of the $D_1,...,D_n$ is
owned by $A$ then $A$ can derive that policy. The notion of
\emph{dataset} of a policy in the article, is thus formalized a bit
stronger here with the notion of \emph{active dataset}, being the
data that is actually affected by the policy. To this end we defined
a relation on $\Gamma$ and $\phi$: $\ADTS{\Gamma}{\phi}$ that holds
iff all data affected by $\phi$, occur in some
$\pred{owns}$-predicate in $\Gamma$. The following rules make up its
definition:
\begin{eqnarray*}
&&\seqinflarge{op\_imp}{\ADTS{\Gamma}{\phi}}
{\ADTS{\Gamma}{(\psi \to \phi)}}\\
&&\seqinflarge{op\_forall}{\ADTS{\Gamma}{\phi(X)}}
{\ADTS{\Gamma}{\forall\phi}}\tt{\ (X\ a\ fresh\ constant)}\\
&&\seqinflarge{op\_says}{\ADTS{\Gamma}{\phi}}
{\ADTS{\Gamma}{\pred{says}(B,\phi,C)}}\\\\
&&\seqinflarge{op\_owns}{\ }
{\ADTS{\Gamma,\pred{owns}(A,D)}{\pred{owns}(B,D)}}\\\\
&&\seqinflarge{op\_print}{\ }
{\ADTS{\Gamma,\pred{owns}(A,D)}{\pred{print}(B,D)}}
\end{eqnarray*}
Where the last one is to show a scenario-specific predicate. Now we
present the standard rules for the sequent calculus:
\begin{eqnarray*}
&&\seqinflarge{init}{}{\entailm{\ }{\Gamma, \phi}{\Delta}{\phi}}
\\\\
&&\seqinflarge{cut}{\entailm{\ }{ \Gamma}{ \Delta}{ \phi} \: \:
\entailm{\ }{\Gamma ' ,\phi}{\Delta '}{\psi}}{\entailm{ A}{
\Gamma,\Gamma '}{\Delta,\Delta '}{\psi}}
\\\\
&&\seqinflarge{and\_l1}{\entailm{\ }{\Gamma,
\phi}{\Delta}{\phi'}}{\entailm{\ }{ \Gamma,(\phi \wedge
\psi)}{\Delta}{\phi'}}
\\\\
&&\seqinflarge{and\_l2}{\entailm{\ }{\Gamma,
\psi}{\Delta}{\phi'}}{\entailm{\ }{\Gamma,(\phi \wedge
\psi)}{\Delta} {\phi'}}
\\\\
&&\seqinflarge{and\_r}{\entailm{\ }{\Gamma}{\Delta}{\phi} \ \
\entailm{\ }{\Gamma '}{\Delta '}{\psi}}{\entailm{\ }{\Gamma,\Gamma
'}{\Delta, \Delta'}{ (\phi \wedge \psi)}}
\\\\
&&\seqinflarge{imp\_l}{\entailm{\ }{\Gamma}{\Delta}{\phi} \: \:
\entailm{\ }{\Gamma ',\phi'}{\Delta '}{\psi}}{\entailm{\
}{\Gamma,\Gamma ',(\phi \to \phi')}{\Delta,\Delta '}{\psi}}
\\\\
&&\seqinflarge{imp\_r}{\entailm{\
}{\Gamma,\phi}{\Delta}{\psi}}{\entailm{\ }{\Gamma}{\Delta}{(\phi \to
 \psi)}}
 \end{eqnarray*}
We need similar left and right rules for the $\limp$ and $\mimp$
operators. Recall that use-many obligations go into the unrestricted
context, while use-once obligations go into the linear context. Here
are the two pairs:
\begin{eqnarray*}
&&\seqinflarge{!imp\_l}{\entailm{\ }{\Gamma}{\Delta}{(\xi\ \limp \
\phi)}} {\entailm{\ }{\Gamma}{\Delta,\xi}{\phi}}
\\\\
&&\seqinflarge{!imp\_r}{\entailm{\
}{\Gamma}{\Delta}{\phi}}{\entailm{\ }{\Gamma}{\Delta}{(\xi \limp
\phi)}}
\\\\
&&\seqinflarge{?imp\_l}{\entailm{\ }{\Gamma}{\Delta}{(\xi\mimp
\phi)}}{\entailm{\ }{\Gamma,\xi}{\Delta}{\phi}}
\\\\
&&\seqinflarge{?imp\_r}{\entailm{\
}{\Gamma}{\Delta}{\phi}}{\entailm{\ }{\Gamma}{\Delta}{(\xi \mimp
\phi)}}
\end{eqnarray*}
In Twelf we coded twice the following $\forall$ -left and $\forall$
-right rules; one for agents, one for data. But not for actions or
policies.
\begin{eqnarray*}
&&\seqinflarge{forall\_l}{\entailm{\
}{\Gamma,\phi(X)}{\Delta}{\psi}} {\entailm{\
}{\Gamma,\forall\phi}{\Delta}{\psi}}
\\\\
&&\seqinflarge{forall\_r}{ \entailm{\
}{\Gamma}{\Delta}{\phi(X)}}{\entailm{\ }{\Gamma}{\Delta}
{\forall\phi}}\tt{\ (X\ a\ fresh\ constant)}\\
\end{eqnarray*}

Finally, we have the structural rules for the unrestricted and the
linear contexts. The linear context doesn't allow for contraction.
\begin{eqnarray*}
&&\seqinflarge{w\_l}{\entailm{\ }{\Gamma}{\Delta}{\phi}}{\entailm{\
}{\Gamma,\psi}{\Delta}{\phi}}
\\\\
&&\seqinflarge{w\_l\_act}{\entailm{\
}{\Gamma}{\Delta}{\phi}}{\entailm{\ }{\Gamma}{\Delta, \xi}{\phi}}
\\\\
&&\seqinflarge{contr\_l}{\entailm{\
}{(\Gamma,\phi),\phi}{\Delta}{\psi}}{\entailm{\
}{\Gamma,\phi}{\Delta}{\psi}}
\\\\
&&\seqinflarge{perm\_l}{\entailm{\ }{\Gamma, \phi, \phi', \Gamma
'}{\Delta}{\psi}}{\entailm{\ }{\Gamma, \phi', \phi, \Gamma
'}{\Delta}{\psi}}
\\\\
&&\seqinflarge{perm\_act}{\entailm{\ }{\Gamma}{\Delta,
\xi,\xi',\Delta'}{\phi}}{\entailm{\ }{\Gamma}{\Delta, \xi',
\xi,\Delta'}{\phi}}
\end{eqnarray*}
Which wraps up the list of rules. We now show some examples of
proofs in this notation.

\subsection{Example: Creating and consuming a policy} Let's draw the
proof-tree of example 2a in this notation. We use abbreviations in
this example:
\begin{eqnarray*}
&&\phi = \forall\psi \qquad
\psi(x) = (\psi_1(x) \to \psi_2)\\
&&\psi_1(x) = \pred{rel}(d,x)\qquad
\psi_2 = \pred{print}(b,d)\\
&&\gamma=\gamma_0,\pred{owns}(a,d) \qquad \gamma' =
\gamma_0,\psi_1(d')
\end{eqnarray*}
In words: Agent $a$ proves that she can say policy $\phi$ to agent
$b$.
\[
\seqinf{OBS\_ACT}{
   \seqinf{cut}{
       \seqinf{DER\_POL}
                {
                \seqinf{op\_says}{
                    \seqinf{op\_print}{\
                    }{\ADTS{\gamma}{\psi_2}}
                    }{\ADTS{\gamma}{\pred{says}(a,\psi_2,b)}}
                }
                {\entailm{\ }{\gamma}{\delta_0}{\pred{says}(a,\psi_2,b)}}
                \quad
                   \seqinf{REFINE}{
                       \entailm{\ }{\gamma_0,\psi_2}{\delta_0}{\phi}}{
                         \entailm{\ }{\gamma_0,\pred{says}(a,\psi_2,b)}{\delta_0}
                                {\pred{says}(a,\phi,b)}}
       }{\entailm{\ }{\gamma}{\delta_0}{\pred{says}(a,\phi,b)}}
    }{\entailm{\ }{\gamma_0,\action{creates}(a,d)}{\delta_0}
                    {\pred{says}(a,\phi,b)}}
\]
Please note that the use of both the {\tt REFINE} and the {\tt
DER\_POL}-rule, and thus the {\tt cut}-rule, is only done to stay
close to the natural deduction style proof given earlier in the
article (see Table \ref{tabl}). In fact, by using only the {\tt
DER\_POL}-rule one could derive the same permission. The premise of
the {\tt REFINE}-rule is easily proven:
\[
            \seqinf{forall\_r}{
                    \seqinf{imp\_r}{
                        \seqinf{w\_l}{
                                \seqinf{init}
                                    {\ }{
                                        \entailm{\ }{\gamma_0,\psi_2}{\delta_0}{\psi_2}
                                    }}{\entailm{\ }{\gamma_0,\psi_2,\psi_1(y)}{\delta_0}{\psi_2}
                            }}{\entailm{\ }{\gamma_0,\psi_2}{\delta_0}{(\psi_1(y)\to\psi_2)}}
                }{\entailm{\
                }{\gamma_0,\psi_2}{\delta_0}{\forall\psi}}
\]
Now agent $b$, who receives the mentioned policy, proves that he has
the permission to print - using the evidence of the communication by
$a$ and the assertion on $d'$ (inside $\gamma'$) which is asserted
by $b$'s environment.
\[
\seqinf{OBS\_ACT}{
    \seqinf{SAY}
        {\seqinf{forall\_l}
            {\seqinf{imp\_l}
                {
                    \seqinf{init}
                        {\ }
                        {\entailm{\ }{\gamma'}{\delta_0}{\psi_1(d')}}
                    \qquad
                    \seqinf{init}
                        {\ }
                        {\entailm{\ }{\gamma_0,\psi_2}{\delta_0}{\psi_2}}
                }{\entailm{\ }{\gamma',(\psi_1(d')\to\psi_2)}{\delta_0}{\psi_2}}}
            {\entailm{\ }{\gamma',\forall\psi}{\delta_0}{\psi_2}}}
        {\entailm{\ }{\gamma',\pred{says}(a,\phi,b)}{\delta_0}{\psi_2}}}
    {\entailm{\ }{\gamma',\action{comm}(a,b,\phi)}{\delta_0}{\psi_2}}
\]
\subsection{Example: Fulfilling use-once obligations} Finally let's
see a policy with $\limp$ in it. The drink-beer example is fine.
Suppose the bartender, $a$, has communicated the policy $\phi$ to a
customer, $b$. The customer has to prove
$po(drunk(b,\text{beer}))=drink(b,\text{beer})$. The abbreviations
are:
\begin{eqnarray*}
&&\phi = \forall \psi \qquad
\psi(x) = (\psi_1(x) \limp \psi_2(x))\\
&&\psi_1(x) = \action{paid}(x,\text{5\$})\qquad
\psi_2(x) = \pred{drink}(x,\text{beer})\\
&&\xi = \action{comm}(a,b,\phi) \qquad \xi' = \action{paid}(b,5\$)
\end{eqnarray*}
Now agent $b$ uses the evidence of the communication and the
obligation $\action{paid}(b,\text{5\$})$ to prove that he is allowed
to drink one beer having paid 5\$.
\[
\seqinf{OBS\_ACT}{
    \seqinf{SAY}
        {\seqinf{forall\_l}
            {\seqinf{!imp\_l}
                {
                    \seqinf{init}
                        {\ }
                        {\entailm{\ }{\gamma_0,\psi(b)}{\delta_0}{(\psi_1(b)\limp\psi_2(b))}}
                }{\entailm{\ }{\gamma_0,\psi(b)}{\delta_0,\xi'}{\psi_2(b)}}}
            {\entailm{\ }{\gamma_0,\forall\psi}{\delta_0,\xi'}{\psi_2(b)}}}
        {\entailm{\ }{\gamma_0,\pred{says}(a,\forall\psi,b)}{\delta_0,\xi'}{\psi_2(b)}}
    }
    {\entailm{\ }{\gamma_0,\xi}{\delta_0,\xi'}{\psi_2(b)}}
\]

%\end{document}

cs0502091.extracted_bib
\begin{thebibliography}{10}

\bibitem{Aba03}
M.~Abadi.
\newblock Logic in access control.
\newblock In {\em Proc. 8th Annual IEEE Symposium on Logic in Computer Science
  (LICS)}, pages 228--233. IEEE Computer Society Press, 2003.

\bibitem{AF99}
A.~W. Appel and E.~W. Felten.
\newblock Proof-carrying authentication.
\newblock In G.~Tsudik, editor, {\em Proc of the 6th Conference on Computer and
  Communications Security}. ACM Press, 1999.

\bibitem{AHKS02}
P.~Ashley, S.~Hada, G.~Karjoth, and M.~Schunter.
\newblock E-p3p privacy policies and privacy authorization.
\newblock In P.~Samarati, editor, {\em Proc.~of the ACM workshop on Privacy in
  the Electronic Society (WPES 2002)}, pages 103--109. ACM Press, 2002.

\bibitem{BCFP03}
E.~Bertino, B.~Catania, E.~Ferrari, and P.~Perlasca.
\newblock A logical framework for reasoning about access control models.
\newblock {\em ACM Transactions on Information and System Security (TISSEC)},
  pages 71--127, 2003.

\bibitem{Cho03a}
C.~N. Chong, R.~Corin, S.~Etalle, P.~H. Hartel, W.~Jonker, and Y.~W. Law.
\newblock {LicenseScript}: {A} novel digital rights language and its semantics.
\newblock In K.~Ng, C.~Busch, and P.~Nesi, editors, {\em 3rd Int. Conf. on Web
  Delivering of Music ({WEDELMUSIC})}, pages 122--129. IEEE Computer Society
  Press, 2003.

\bibitem{Cor04b}
R.~Corin, S.~Etalle, J.~I. den Hartog, G.~Lenzini, and I.~Staicu.
\newblock {A} logic for auditing accountability in decentralized systems.
\newblock In T.~Dimitrakos and F.~Martinelli, editors, {\em Proc. of the second
  IFIP Workshop on Formal Aspects in Security and Trust ({FAST})}, volume 173,
  page to appear. Springer Verlag, 2004.

\bibitem{DeT02}
John {DeT}reville.
\newblock Binder, a logic-based security language.
\newblock In {\em Proceedings of the {IEEE} Symposium on Research in Security
  and Privacy}, pages 105--113. {IEEE} Computer Society Press, 2002.

\bibitem{JSSE97}
S.~Jajodia, P.~Samarati, V.~S. Subrahmanian, and E.~Bertino.
\newblock A unified framework for enforcing multiple access control policies.
\newblock In J.~Peckham, editor, {\em SIGMOD 1997, Proc. International
  Conference on Management of Data}, pages 474--485. ACM Press, 1997.

\bibitem{LMW02}
N.\ Li, J.\ Mitchell, and W.\ Winsborough.
\newblock Design of a role-based trust-management framework.
\newblock In {\em Proc. of the {IEEE} Symposium on Research in Security and
  Privacy}, pages 114--130. {IEEE} Computer Society Press, 2002.

\bibitem{necula98compiling}
G.~C. Necula.
\newblock {\em Compiling with Proofs}.
\newblock PhD thesis, School of Computer Science, Carnegie Mellon University,
  Pittsburgh, PA, 1998.

\bibitem{PS02}
J.~Park and R.~Sandhu.
\newblock Towards usage control models: Beyond traditional access control.
\newblock In R.~Sandhu, editor, {\em Proc.\ of the Seventh {ACM} Symposium on
  Access Control Models and Technologies ({SACMAT}-02)}, pages 57--64. ACM
  Press, 2002.

\bibitem{pfenning91logic}
F.~Pfenning.
\newblock Logic programming in the {LF} logical framework.
\newblock In G.~Huet and G.~Plotkin, editors, {\em Logical Frameworks}, pages
  149--181. Cambridge University Press, 1991.

\bibitem{pfenning99system}
F.~Pfenning and C.~Sch{\"u}rmann.
\newblock System description: Twelf --- {A} meta-logical framework for
  deductive systems.
\newblock In H.~Ganzinger, editor, {\em Proc. of the 16th International
  Conference on Automated Deduction ({CADE}-16)}, pages 202--206.
  Springer-Verlag, 1999.

\bibitem{Sam01}
P.~Samarati and S.~De~Capitani di~Vimercati.
\newblock Access control: policies, models, and mechanisms.
\newblock In R.~Focardi and R.~Gorrieri, editors, {\em Foundations of Security
  Analysis and Design, LNCS}, volume 2171, pages 137--196. Springer-Verlag,
  2001.

\bibitem{SP03}
R.~Sandhu and J.~Park.
\newblock Usage control: {A} vision for next generation access control.
\newblock In V.~Gorodetsky, L.~J. Popyack, and V.~A. Skormin, editors, {\em
  Proc.\ Second International Workshop on Mathematical Methods, Models, and
  Architectures for Computer Network Security MMM-ACNS}, volume 2776 of {\em
  LNCS}, pages 17--31. Springer-Verlag, 2003.

\bibitem{SS94}
R.~Sandhu and P.~Samarati.
\newblock Access control: Principles and practice.
\newblock {\em IEEE Communications Magazine}, 32(9):40--48, 1994.

\bibitem{p3p}
W3C.
\newblock A p3p preference exchange language 1.0 (appel1.0).
\newblock www.w3.org/TR/P3P-preferences, 2002.

\bibitem{Wang02}
X.~Wang, G.~Lao, T.~{De Martini}, H.~Reddy, M.~Nguyen, and E.~Valenzuela.
\newblock {XrML}: {eXtensible} rights markup language.
\newblock In M.~Kudo, editor, {\em Proc. 2002 {ACM} workshop on {XML} security
  ({XMLSEC}-02)}, pages 71--79. ACM Press, 2002.

\bibitem{WAN04}
N.~Whitehead, M.~Abadi, and G.~C. Necula.
\newblock By reason and authority: A system for authorization of proof-carrying
  code.
\newblock In {\em Proc. of the 17th Computer Security Foundations Workshop},
  pages 236--250. {IEEE} Computer Society Press, 2004.

\end{thebibliography}