Unguessable Atoms: A Logical Foundation for Security

  • Mark Bickford
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)


We show how a type of atoms, which behave like urelements, and a new proposition that expresses the independence of a term from an atom can be added to any logical system after imposing minor restrictions on definitions and computations. Working in constructive type theory, we give rules for the independence proposition and show how cryptographic protocols can be modeled as automata exchanging atoms. This model provides a unifying framework for reasoning about security and allows us to combine a general model of computation with a simple model of acquisition of secret information. As an application, we prove a fundamental property of nonces that justifies the axioms for nonces used in the protocol composition logic (PCL) of Datta, Derek, Mitchell and Roy. The example shows that basic security properties are naturally expressed in terms of independence and the causal ordering of events. The rules and example proofs are fully implemented in the Nuprl proof development system.


Computation System Symbolic Model Cryptographic Protocol Logical Foundation Virtual Server 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Allen, S.F.: A non-type-theoretic definition of martin-löf’s types. In: Proceedings of Second IEEE Symposium on Logic in Computer Science, pp. 215–224 (1987)Google Scholar
  2. 2.
    Allen, S.F.: An Abstract Semantics for Atoms in Nuprl. Cornell Tech Report TR2006-2032 (2006)Google Scholar
  3. 3.
    Bickford, M.: Event systems. Nuprl Math Library Book webpage (2003)Google Scholar
  4. 4.
    Bickford, M., Constable, R.L.: A logic of events. Technical Report TR2003-1893, Cornell University (2003)Google Scholar
  5. 5.
    Blass, A., Gurevich, Y., Shelah, S.: Choiceless polynomial time. Pure and Applied Logic 100, 141–187 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Constable, R.L.: Types in logic, mathematics and programming. In: Buss, S.R. (ed.) Handbook of Proof Theory, pp. 683–786. Elsevier Science B.V, Amsterdam (1998)CrossRefGoogle Scholar
  7. 7.
    Datta, A., Derek, A., Mitchell, J., Ramanathan, A., Scedrov, A.: Games and the impossibility of realizable ideal functionality. In: Proceedings of 16th IEEE Computer Security Foundations Workshop, pp. 360–379 (March 2006)Google Scholar
  8. 8.
    Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol composition logic (pcl). In: Plotkin Festschrift, G.D. (ed.) Electronic Notes in Theoretical Computer Science (to appear, 2007)Google Scholar
  9. 9.
    Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Multiset rewriting and the complexity of bounded security protocols (2002)Google Scholar
  11. 11.
    Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13, 341–363 (2002)zbMATHCrossRefGoogle Scholar
  12. 12.
    Goldreich, O.: Foundations of Cryptography. Basic Tools, vol. 1. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  13. 13.
    Martin-Löf, P.: Constructive mathematics and computer programming. In: 6th International Congress for Logic, Methodology, and Philosophy of Science, North Holland, Amsterdam (1982)Google Scholar
  14. 14.
    Meadows, C.A.: Formal verification of cryptographic protocols: A survey. In: ASIACRYPT: Advances in Cryptology – ASIACRYPT: International Conference on the Theory and Application of Cryptology. LNCS. Springer, Heidelberg (1994)Google Scholar
  15. 15.
    Millen, J.K., Rueß, H.: Protocol-independent secrecy. In: IEEE Symposium on Security and Privacy, pp. 110–209 (2000)Google Scholar
  16. 16.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic, vol. 2283. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  17. 17.
    Paulson,: Proving security protocols correct. In: LICS: IEEE Symposium on Logic in Computer Science (1999)Google Scholar
  18. 18.
    Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1-2), 85–128 (1998)Google Scholar
  19. 19.
    Pfenning, F., Schürmann, C.: Twelf — a meta-logical framework for deductive systems, pp. 202–206 (1999)Google Scholar
  20. 20.
    Thayer, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. Journal of Computer Security 7(1) (1999)Google Scholar
  21. 21.
    Troelstra, A.: Choice Sequences. Clarendon Press, Oxford (1977)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Mark Bickford
    • 1
  1. 1.ATC-NY and Cornell University Computer ScienceIthacaUSA

Personalised recommendations