Resolving the Tension between Integrity and Security Using a Theorem Prover.

Subhasish Mazumdar, David W. Stemple, Tim Sheard: Resolving the Tension between Integrity and Security Using a Theorem Prover. SIGMOD Conference 1988: 233-242
  author    = {Subhasish Mazumdar and
               David W. Stemple and
               Tim Sheard},
  editor    = {Haran Boral and
               Per-{\AA}ke Larson},
  title     = {Resolving the Tension between Integrity and Security Using a
               Theorem Prover},
  booktitle = {Proceedings of the 1988 ACM SIGMOD International Conference on
               Management of Data, Chicago, Illinois, June 1-3, 1988},
  publisher = {ACM Press},
  year      = {1988},
  pages     = {233-242},
  ee        = {, db/conf/sigmod/MazumdarSS88.html},
  crossref  = {DBLP:conf/sigmod/88},
  bibsource = {DBLP,}


Some information in databases and knowledge bases often needs to be protected from disclosure to certain users. Traditional solutions involving multi-level mechanisms are threatened by the user's ability to infer higher level information from the semantics of the application. We concentrate on the revelation of secrets through a user running transactions in the presence of database integrity constraints. We develop a method of specifying secrets formally that not only exposes a useful structure and equivalence among secrets but also allows a theorem prover to detect certain security lapses during transaction compilation time.

Copyright © 1988 by the ACM, Inc., used by permission. Permission to make digital or hard copies is granted provided that copies are not made or distributed for profit or direct commercial advantage, and that copies show this notice on the first page or initial screen of a display along with the full citation.

ACM SIGMOD Anthology

Online Version (ACM WWW Account required): Full Text in PDF Format

CDROM Version: Load the CDROM "Volume 1 Issue 2, SIGMOD '75-'92" and ...

DVD Version: Load ACM SIGMOD Anthology DVD 1" and ... BibTeX

Printed Edition

Haran Boral, Per-Åke Larson (Eds.): Proceedings of the 1988 ACM SIGMOD International Conference on Management of Data, Chicago, Illinois, June 1-3, 1988. ACM Press 1988 BibTeX , SIGMOD Record 17(2), June 1988

Online Edition: ACM Digital Library


[Bancilhon and Spyratos 77]
François Bancilhon, Nicolas Spyratos: Protection of Information in Relational Data Bases. VLDB 1977: 494-500 BibTeX
[Boyer and Moore 79]
[Casanova and Bernstein 80]
Marco A. Casanova, Philip A. Bernstein: A Formal System for Reasoning about Programs Accessing a Relational Database. ACM Trans. Program. Lang. Syst. 2(3): 386-414(1980) BibTeX
[Denning et al. 79]
Dorothy E. Denning, Peter J. Denning, Mayer D. Schwartz: The Tracker: A Threat to Statistical Database Security. ACM Trans. Database Syst. 4(1): 76-96(1979) BibTeX
[Dobkin et al. 79]
David P. Dobkin, Anita K. Jones, Richard J. Lipton: Secure Databases: Protection Against User Influence. ACM Trans. Database Syst. 4(1): 97-106(1979) BibTeX
[Gardarin and Melkanoff 79]
Georges Gardarin, Michel A. Melkanoff: Proving Consistency of Database Transactions. VLDB 1979: 291-298 BibTeX
[Fernandez et al. 81]
[Henschen et al. 84]
Lawrence J. Henschen, William McCune, Shamim A. Naqvi: Compiling Constraint-Checking Programs from First-Order Formulas. Advances in Data Base Theory 1982: 145-169 BibTeX
[Nicolas 82]
Jean-Marie Nicolas: Logic for Improving Integrity Checking in Relational Data Bases. Acta Inf. 18: 227-253(1982) BibTeX
[Sicherman et al. 83]
George L. Sicherman, Wiebren de Jonge, Reind P. van de Riet: Answering Queries Without Revealing Secrets. ACM Trans. Database Syst. 8(1): 41-59(1983) BibTeX
[Morgenstern 87]
Matthew Morgenstern: Security and Inference in Multilevel Database and Knowledge-Base Systems. SIGMOD Conference 1987: 357-373 BibTeX
[Sheard and Stemple 86]
Tim Sheard, David W. Stemple: Automatic Verification of Database Transaction Safety. ACM Trans. Database Syst. 14(3): 322-368(1989) BibTeX
[Stemple and Sheard 85]
[Stemple and Sheard 87]
David W. Stemple, Tim Sheard: Construction and Calculus of Types for Database Systems. DBPL 1987: 3-22 BibTeX
[Stemple et al. 86]
[Stemple et al. 87]
David W. Stemple, Subhasish Mazumdar, Tim Sheard: On the Modes and Meaning of Feedback to Transaction Designers. SIGMOD Conference 1987: 374-386 BibTeX

Referenced by

  1. Keishi Tajima: Static Detection of Security Flaws in Object-Oriented Databases. SIGMOD Conference 1996: 341-352
ACM SIGMOD Anthology - DBLP: [Home | Search: Author, Title | Conferences | Journals]
ACM SIGMOD Anthology: Copyright © by ACM (, Corrections:
DBLP: Copyright © by Michael Ley (, last change: Sat May 16 23:39:54 2009