Verifying secrets and relative secrecy
- 5 January 2000
- proceedings article
- Published by Association for Computing Machinery (ACM)
- p. 268-276
- https://doi.org/10.1145/325694.325729
Abstract
The article of record as published may be located at http://dx.doi.org/10.1145/325694.325729Systems that authenticate a user based on a shared secret (such as a password or PIN) normally allows anyone to query whether the secret is a given value. For example, an ATM machine allows one to ask whether a string is the secret PIN of a (lost or stolen) ATM card. Yet such queries are prohibited in any model whose programs satisfy an information flow property like Noninterference. But there is a complexity-based justification for allowing these queries. A type system is given that provides the access control needed to prove that no well-tyoed program can leak secrets in polynomial time, or even leak them with nonnegligible probability if secrets are of sufficient length and randomly chosen. However, there are well-typed deterministic programs in a synchronous concurrent model capable of leaking secrets in linear timeKeywords
This publication has 5 references indexed in Scilit:
- JFlowPublished by Association for Computing Machinery (ACM) ,1999
- A probabilistic poly-time framework for protocol analysisPublished by Association for Computing Machinery (ACM) ,1998
- Secure information flow in a multi-threaded imperative languagePublished by Association for Computing Machinery (ACM) ,1998
- Security Policies and Security ModelsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1982
- Relativizations of the $\mathcal{P} = ?\mathcal{NP}$ QuestionSIAM Journal on Computing, 1975