%%
\documentclass[envcountsame,orivec]{llncs}
% \documentclass[a4paper,11pt]{article}
%\documentclass[twocolumn,a4paper,11pt]{article}

\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
% \usepackage{exptrees}
\usepackage{url}
\usepackage{proof}

\renewcommand{\today}{\number\day\ 
  \ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \ \number\year}

\setcounter{secnumdepth}2
\setcounter{tocdepth}2

% \newtheorem{theorem}{Theorem}[section]

% \newcommand{\qed}{}

% \newenvironment{proof}{
 % \noindent{\bf Proof:}}{\mbox{\bf Q.E.D.}\vspace{1ex}}

% \newtheorem{definition}{Definition}[section]

% \newtheorem{lemma}{Lemma}[section]

% \newtheorem{corollary}{Corollary}[section]
    
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble
\newcommand\cfile{}

\newcommand\comment[1]{} 
\newcommand\cc[1]{#1} % for label names 

\renewcommand\theenumi{(\alph{enumi})}
\renewcommand\labelenumi{\theenumi}
\renewcommand\theenumii{(\roman{enumii})}
\renewcommand\labelenumii{\theenumii}

\newcommand\src[1]{source file \texttt{#1}}
\newcommand\apsrc[1]{Appendix \ref{app:code}}
\newcommand\seesrc[1]{(see source file \texttt{#1})}
\newcommand\insrc[1]{in source file \texttt{#1}}
\newcommand\page[1]{page~\pageref{#1}}
\newcommand\fig[1]{Fig.~\ref{fig:#1}}
\newcommand\ch[1]{Chapter~\ref{ch:#1}}
\newcommand\tbl[1]{Table~\ref{tbl:#1}}
\newcommand\thrm[1]{Theorem~\ref{thrm:#1}}
\newcommand\lem[1]{Lemma~\ref{lem:#1}}
\newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}}
%\newcommand\M{$\mathcal M$}
\newcommand\MP{\ensuremath{\mathcal P}}
\newcommand\MQ{\ensuremath{\mathcal Q}}
\newcommand\MR{\ensuremath{\mathcal R}}
\newcommand\M{\ensuremath{\mathcal M}}
\newcommand\Mp{$\mathcal M'$}
\newcommand\up[1]{\vspace{-#1ex}} 
\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree
\newcommand\cut{(\emph{cut})}


\newcommand\pairM{\ensuremath{\langle M_a, M_b \rangle}} 
\newcommand\pairN{\ensuremath{\langle N_a, N_b \rangle}} 
\newcommand\encM{\ensuremath{\{ M_p \}_{M_k}}}
\newcommand\encN{\ensuremath{\{ N_p \}_{N_k}}}
\newcommand\encQ{\ensuremath{\{ Q_p \}_{Q_k}}}
\newcommand\encR{\ensuremath{\{ R_p \}_{R_k}}}

\def\seqsym{\vdash}

\newcommand\Ne{\ensuremath{\mathcal N^=}}
\newcommand\irred[1]{#1 \!\! \Downarrow}
\newcommand\GammaR{\ensuremath{\Gamma \!\! \Downarrow}}
\newcommand\RNe[1]{\ensuremath{#1 \!\! \Downarrow \setminus \Ne}}
\newcommand\GammaRNe{\ensuremath{\GammaR \setminus \Ne}}


\def\rna{{\mathbf a}}
\def\rnb{{\mathbf b}}
\def\rnc{{\mathbf c}}
\def\rnd{{\mathbf d}}
\def\rne{{\mathbf e}}
\def\rnk{{\mathbf k}}
\def\rnl{{\mathbf l}}

\pagestyle{plain}

% \input{app_labels} % for references to Appendix if Appendix not included

\begin{document}

\title{Decidability of Bi-trace Consistency}

\author{
 Jeremy E.\ Dawson
%\thanks{Supported by an Australian Research Council Large Grant}
 \ \ and \ \
 Alwen Tiu
%\thanks{Supported by an Australian Research Council Large Grant}
}
\institute{
Logic and Computation Group
\\College of Engineering and Computer Science
\\ Australian National University
\\ Canberra ACT 0200, Australia
\\ \url{http://users.rsise.anu.edu.au/~jeremy/} 
\ \ \url{http://users.rsise.anu.edu.au/~tiu/}
}

\date{}
%% Title 
\maketitle


\begin{abstract}

YET TO CHANGE FROM TPHOLS 2009 PAPER
We consider a formalisation of a notion of observer (or intruder) theories, commonly
used in symbolic analysis of security protocols.  
An observer theory describes the knowledge and capabilities of an observer,
and can be given a formal account using deductive systems, such
as those used in various ``environment-sensitive'' bisimulation for
process calculi, e.g., the spi-calculus. 
Two notions are critical to the correctness of such formalisations and 
the effectiveness of symbolic techniques based on them: decidability of 
message deduction by the observer and consistency 
of a given observer theory. We consider a formalisation, in Isabelle/HOL,
of both notions based on an encoding of observer theories as 
pairs of symbolic traces. 
This encoding has recently been used in a theory of 
open bisimulation for the spi-calculus. 
We machine-checked some important properties, including decidability of 
observer deduction and consistency, and some key steps which are 
crucial to the automation of open bisimulation checking for 
the spi-calculus, and highlight some 
novelty in our Isabelle/HOL formalisations of decidability proofs.
\end{abstract}


%% Here begins the main text

% (* Alwen's commands *)
\newcommand\spr[2]{\langle #1, #2 \rangle}
\newcommand\enc[2]{\{#1\}_{#2}}
\def\eqm{\leftrightarrow}

\input{intro}
\input{fsrs}
\input{cons}
\input{concl}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here begins the end matter

%\bibliographystyle{plain}
%\bibliography{spi}

\begin{thebibliography}{10}

\bibitem{abadi01popl}
Mart\'{\i}n Abadi and C{\'e}dric Fournet.
\newblock Mobile values, new names, and secure communication.
\newblock In {\em POPL}, pages 104--115, 2001.

\bibitem{abadi98njc}
Mart\'{\i}n Abadi and Andrew~D. Gordon.
\newblock A bisimulation method for cryptographic protocols.
\newblock {\em Nord. J. Comput.}, 5(4):267--303, 1998.

\bibitem{abadi99ic}
Martin Abadi and Andrew~D. Gordon.
\newblock A calculus for cryptographic protocols: {The} spi calculus.
\newblock {\em Information and Computation}, 148(1):1--70, 99.

\bibitem{baudet07phd}
Mathieu Baudet.
\newblock {\em S{\'e}curit{\'e} des protocoles cryptographiques: aspects
  logiques et calculatoires}.
\newblock PhD thesis, {\'E}cole {N}ormale {S}up{\'e}rieure de {C}achan,
  {F}rance, 2007.

\bibitem{boreale}
Michele Boreale.
\newblock Symbolic trace analysis of cryptographic protocols.
\newblock In {\em Proceedings of ICALP 2001}, volume 2076 of {\em LNCS}, pages
  667 -- 681. Springer-Verlag, 2001.

\bibitem{boreale-siam}
Michele Boreale, Rocco~De Nicola, and Rosario Pugliese.
\newblock Proof techniques for cryptographic processes.
\newblock {\em SIAM J. Comput.}, 31(3):947--986, 2001.

\bibitem{borgstrom04concur}
Johannes Borgstr{\"o}m, S{\'e}bastien Briais, and Uwe Nestmann.
\newblock Symbolic bisimulation in the spi calculus.
\newblock In {\em CONCUR}, vol. 
  3170 of {\em LNCS}, pp 161--176. Springer, 2004.

\bibitem{borgstrom05}
Johannes Borgstr{\"o}m and Uwe Nestmann.
\newblock On bisimulations for the spi calculus.
\newblock {\em Mathematical Structures in Computer Science}, 15(3):487--552,
  2005.

\bibitem{dawson-gore-gls-ca}
J.~E. Dawson and R.~Gor{\'e}.
\newblock Formalising cut-admissibility for provability logic.
\newblock Submitted, 2009.

\bibitem{dawson-tiu-fotesb}
J.~E. Dawson and A.~Tiu.
{Formalising Observer Theory for Environment-Sensitive Bisimulation}.
\newblock In {\em TPHOLs 2009}, vol. 
  5674 of {\em LNCS}, pp 180--195. Springer, 2009.


\bibitem{dolevyao}
D.~Dolev and A.~Yao.
\newblock On the security of public-key protocols.
\newblock {\em IEEE Transactions on Information Theory}, 2(29), 1983.

\bibitem{kahsai08}
Temesghen Kahsai and Marino Miculan.
\newblock Implementing spi calculus using nominal techniques.
\newblock In {\em CiE}, volume 5028 of {\em LNCS}, pages 294--305. Springer,
  2008.

\bibitem{milner92icII}
Robin Milner, Joachim Parrow, and David Walker.
\newblock A calculus of mobile processes, {Part II}.
\newblock {\em Information and Computation}, pages 41--77, 1992.

\bibitem{sangiorgi96acta}
Davide Sangiorgi.
\newblock A theory of bisimulation for the pi-calculus.
\newblock {\em Acta Inf.}, 33(1):69--97, 1996.

\bibitem{tiu-trace-based-bisim-abs}
Alwen Tiu.
\newblock A trace based bisimulation for the spi calculus: An extended
  abstract.
\newblock In {\em Proc. APLAS}, vol. 4807 of {\em LNCS}, pages
  367--382. Springer, 2007.

\bibitem{tiu-trace-based-bisim-full}
Alwen Tiu.
\newblock A trace based bisimulation for the spi calculus.
\newblock Preprint, available from \url{http://arxiv.org/pdf/0901.2166v1},
  2009.

\bibitem{tiu-gore-intruder}
Alwen Tiu and Rajeev Gor{\'e}.
\newblock A proof theoretic analysis of intruder theories.
\newblock In {\em Proceedings of RTA 2009}, 2009.
\newblock To appear.

\bibitem{ucb-mech-LF}
Christian Urban, James Cheney, and Stefan Berghofer.
\newblock Mechanizing the metatheory of LF.
\newblock In {\em LICS}, pages 45--56. IEEE Computer Society, 2008.

\end{thebibliography}

% following line needs to be present to get references to Appendix
% if not, uncomment \input{app_labels} at the beginning
% \input{app} % not for proceedings version 
% \input{notes} % not for proceedings or online version 

\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
