Abstract
Security is an important non-functional requirement for nearly any software system. There should not be any room for security errors in software systems like databases and other critical systems, where data is stored and should be retrieved through authentication. Informal specifications are easy to write and read, but they suffer from contradiction and ambiguities. Formal Specifications are the most efficient and flawless way of defining security constraints. This project specifies secure query processing in deductive database systems using the well know formal language Z. The system state and invariants of deductive database systems are formally modeled. The security constraints of table manipulation operations and other administrative operations are formally specified in terms of the preconditions and postconditions of these operations.