@TechReport{	  it:2005-004,
  author	= {Michael Baldamus and Joachim Parrow and Bj{\"o}rn Victor},
  title		= {A Fully Abstract Encoding of the $\pi$-Calculus with Data
		  Terms},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Division of Computer Systems},
  year		= {2005},
  number	= {2005-004},
  month		= feb,
  note		= {Updated April 2005},
  abstract	= {The $\pi$-calculus with data terms ($\pi$T) extends the
		  pure $\pi$-calculus by data constructors and destructors
		  and allows data to be transmitted between agents. It has
		  long been known how to encode such data types in $\pi$, but
		  until now it has been open how to make the encoding
		  \emph{fully abstract}, meaning that two encodings (in
		  $\pi$) are semantically equivalent precisely when the
		  original $\pi$T agents are semantically equivalent. We
		  present a new type of encoding and prove it to be fully
		  abstract with respect to may-testing equivalence. To our
		  knowledge this is the first result of its kind, for any
		  calculus enriched with data terms. It has particular
		  importance when representing security properties since
		  attackers can be regarded as may-test observers. Full
		  abstraction proves that it does not matter whether such
		  observers are formulated in $\pi$ or $\pi$T, both are
		  equally expressive in this respect. The technical new idea
		  consists of encoding data as table entries rather than
		  active processes, and using a firewalled central integrity
		  manager to ensure data security.}
}