Model checking offers a methodology for determining whether a model satisfies a list of correctness requirements. We propose a theory of dependability auditing with model checking based on four principles: (1) The modeling process should be partitioned into computational components and behavioral components as an aid to system understanding; (2) Abstracting from the detail of the actual system design; (3) A language must be available that can represent and evaluate states and processes that evolve over time; (4) Given an adequate model and temporal specifications, a model checker can verify whether or not the input model is a model of that specification: the specification will not fail in the model. We demonstrate this theoretical framework with Web Services and electronic contracting.