We define lambda-seal, an untyped call-by-value lambda-calculus with
primitives for protecting abstract data by _sealing_, and develop a
bisimulation proof method that is sound and complete with respect to
contextual equivalence.  This provides a formal basis for reasoning
about data abstraction in open, dynamic settings where static
techniques such as type abstraction and logical relations are not
applicable.