The authors present a specification and verification method for preventing denial of service in the absence of failure and of integrity violations. They introduce a service-specification model to verify the absence of denial of service. A key component of that model is the separation of the service-sharing mechanism from the service-sharing policy. The authors discuss the need to specify fairness and simultaneity conditions formally within the sharing policy. They argue that, in contrast with other properties, the prevention of denial of service requires specifications of service use. These specifications, or user agreements, are external constraints on service invocations that must be obeyed by all service users. In general, these constraints cannot be converted into internal service-enforced constraints such as those of the service-sharing mechanisms and policies.