Papers by Jonathan Herzog

[1] E. Grunwald, J. Herzog, and C. Steel, ``Using fourier transforms to understand spectral line shapes,'' Journal of Chemical Education, vol. 72, no. 3, pp. 210-214, 1995.
[ bib ]
[2] J. Herzog, C. McLaren, and A. Godbole, ``Generalized k-matches,'' Statistics and Probability Letters, vol. 38, pp. 167-175, 1998.
[ bib ]
Suppose that an urn contains m distinguishable balls, and that these balls are sampled (with replacement), thus generating a sequence of colors. Many questions can be asked about this sequence; the distribution of the time until a color is sampled twice within a memory window of size k (i.e, the waiting time until the first k-match) was derived by Arnold (1972). Next, Burghardt et. al. (1994) proved that the limiting distribution of the number of k-matches in the first n draws is Poisson if k=o(m). An even more general question is discussed here: if, for every draw from the urn, a random k-sample is taken of the previous draws, what is the distribution of the number of generalized k-matches? Our solution resolves a question of Glen Meeden (see Arnold, 1972). Extensions to the case where the k-sample is drawn from the (union of the) past and the future are provided, and the case of non-uniform probabilities is treated.
[3] F. J. Thayer Fabrega, J. Herzog, and J. D. Guttman, ``Strand spaces: Why is a security protocol correct?,'' in 1998 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, May 1998.
[ bib | web page ]
A strand is a sequence of events; it represents either the execution of legitimate party in a security protocol or else a sequence of actions by a penetrator. A strand space is a collection of strands, equipped with a graph structure generated by causal interaction. In this framework, protocol correctness claims may be expressed in terms of the con-nections between strands of different kinds.

In this paper we develop the notion of a strand space. We then prove a generally useful lemma, as a sample result giving a general bound on the abilities of the penetrator in any protocol. We apply the strand space formalism to prove the correctness of the Needham- Schroeder-Lowe protocol. Our approach gives a detailed view of the condi-tions under which the protocol achieves authentication and protects the secrecy of the values exchanged. We also use our proof methods to explain why the original Needham-Schroeder protocol fails.

We believe that our approach is distinguished from other work on protocol verification by the simplicity of the model and the ease of producing intelligible and reliable proofs of protocol correctness even without automated support.

[4] F. J. T. Fabrega, J. Herzog, and J. D. Guttman, ``Strand space pictures,'' in Proceedings, Workship on Formal Methods and Security Protocols, June 1998. Co-located with LICS'98.
[ bib ]
In this paper, we supplement the ``strand space'' proof methods for cryptographic protocols developed in [?] by explaining another, heuristic advantage of the method. Namely, strand spaces help us draw informative pictures of cryptographic protocols, of attacks on protocols, of correctness theorems for protocols, and of crucial steps in the proofs.

As a consequence, it is possible to discover sharper characterizations of the goals of a protocol, and to discover more easily whether those goals are met.

[5] F. J. Thayer Fabrega, J. Herzog, and J. D. Guttman, ``Honest ideals on strand spaces,'' in Proceedings of the 11th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, June 1998.
[ bib | web page ]
In security protocol analysis, it is important to learn general principles that limit the abilities of an attacker, and that can be applied repeatedly to a variety of protocols. We introduce the notion of an ideal-a set of messages closed under encryption and invariant under composition with arbitrary messages-to express such principles.

In conjunction with the strand space formalism, we use the concept of ideals to prove bounds on a penetrator's capabilities, independent of the security protocol being analyzed. From this we prove a number of correctness properties of the Otway Rees protocol, using these results to explain the limitations of the protocol.

[6] F. J. Thayer, J. Herzog, and J. D. Guttman, ``Strand spaces: Proving security protocols correct,'' Journal of Computer Security, vol. 7, no. 2/3, pp. 191-230, 1999.
[ bib | web page ]
A strand is a sequence of events; it represents either an execution by a legitimate party in a security protocol or else a sequence of actions by a penetrator. A strand space is a collection of strands, equipped with a graph structure generated by causal interaction. In this framework, protocol correctness claims may be expressed in terms of the connections between strands of di erent kinds.

Preparing for a first example, the Needham-Schroeder-Lowe protocol, we prove a lemma that gives a bound on the abilities of the penetrator in any protocol. Our analysis of the example gives a detailed view of the conditions under which it achieves authentication and protects the secrecy of the values exchanged. We also use our proof methods to explain why the original Needham-Schroeder protocol fails.

Before turning to a second example, we introduce ideals as a method to prove additional bounds on the abilities of the penetrator. We can then prove a number of correctness properties of the Otway-Rees protocol, and we clarify its limitations.

We believe that our approach is distinguished from other work by the simplicity of the model, the precision of the results it produces, and the ease of developing intelligible and reliable proofs even without automated support.

[7] F. J. Thayer Fabrega, J. Herzog, and J. D. Guttman, ``Mixed strand spaces,'' in Proceedings of the 12th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, June 1999.
[ bib | web page ]
Strand space analysis is a method for stating and proving correctness properties for cryptographic protocols. In this paper we apply the same method to the related problem of mixed protocols, and show that a protocol can remain correct even when used in combination with a range of other protocols.

We illustrate the method with the familiar Otway-Rees protocol. We identify a simple and easily verified characteristic of protocols, and show that the Otway- Rees protocol remains correct even when used in combination with other protocols that have this characteristic.

We also illustrate this method on the Neuman-Stubblebine protocol. This protocol has two parts, an authentication protocol (I) in which a key distribution center creates and distributes a Kerberos-like key, and a reauthentication protocol (II) in which a client resubmits a ticket containing that key. The re-authentication protocol II is known to be flawed. We show that in the presence of protocol II, there are also attacks against protocol I. We then define a variant of protocol II, and prove an authentication property of I that holds even in combination with the modified II.

[8] J. Herzog, ``Computational soundness for formal adversaries,'' Master's thesis, Massachusetts Institute of Technology, October 2002.
[ bib | .ps | .pdf ]
The Dolev-Yao model is a useful and widespread framework in which to analyze security protocols. However, it models the messages of the protocol at a very high level and makes extremely strong assumptions about the power of the adversary. The computational model of cryptography and cryptographic protocols takes a much more low-level view of messages and uses much weaker assumptions. A major result of this work will be the demonstration that certain kinds of computational cryptography can result in an equivalence of sorts between the formal and computational adversary. Specifically, we give an interpretation to the messages of the Dolev-Yao model in terms of computational cryptography. We then define a computational security condition on the powers of the computational adversary, and show that this condition limits the computational adversary to the operations of the Dolev-Yao adversary. Lastly, we show that this security condition is achievable using standard computational cryptographic constructs.
[9] J. Herzog, ``A computational interpretation of dolev-yao adversaries,'' in Proceedings, Workship on Issues in the Theory of Security (WITS'03) (R. Gorrieri, ed.), pp. 146-155, April 2003. Co-located with ETAPS 2003.
[ bib ]
Please see journal version, below
[10] J. Herzog, ``The Diffie-Hellman key-agreement scheme in the strand-space model,'' in 16th Computer Security Foundations Workshop, (Asilomar, CA), pp. 234-247, IEEE CS Press, June 2003.
[ bib | web page ]
The Diffie-Hellman key exchange scheme is a standard component of cryptographic protocols. In this paper, we propose a way in which protocols that use this computational primitive can be verified using formal methods. In particular, we separate the computational aspects of such an analysis from the formal aspects. First, we use Strand Space terminology to define a security condition that summarizes the security guarantees of Diffie-Hellman. Once this property is assumed, the analysis of a protocol is a purely formal enterprise. (We demonstrate the applicability and usefulness of this property by analyzing a sample protocol.) Furthermore, we show that this property is sound in the computational setting by mapping formal attacks to computational algorithms. We demonstrate that if there exists a formal attack that violates the formal security condition, then it maps to a computational algorithm that solves the Diffie-Hellman problem. Hence, if the Diffie-Hellman problem is hard, the security condition holds globally.
[11] J. Herzog, M. Liskov, and S. Micali, ``Plaintext awareness via key registration,'' in Advances in Cryptology - CRYPTO 2003 (D. Boneh, ed.), vol. 2729 of Lecture Notes in Computer Science, pp. 548-564, Springer-Verlag, August 2003.
[ bib | .ps | .pdf ]
In this paper, we reconsider the notion of plaintext awareness. We present a new model for plaintext-aware encryption that is both natural and useful. We achieve plaintext-aware encryption without random oracles by using a third party. However, we do not need to trust the third party: even when the third party is dishonest, we still guarantee security against adaptive chosen ciphertext attacks. We show a construction that achieves this definition under general assumptions. We further motivate this achievement by showing an important and natural application: giving additional real-world meaningfulness to the Dolev-Yao model.
[12] R. Canetti and J. Herzog, ``Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange).'' Cryptology ePrint Archive, Report 2004/334, 2004.
[ bib | web page ]
Symbolic analysis of cryptographic protocols is dramatically simpler than full-fledged cryptographic analysis. In particular, it is readily amenable to automation. However, symbolic analysis does not a priori carry any cryptographic soundness guarantees. Following recent work on cryptographically sound symbolic analysis, we demonstrate how Dolev-Yao style symbolic analysis can be used to assert the security of cryptographic protocols within the universally composable (UC) security framework. Consequently, our methods enable security analysis that is completely symbolic, and at the same time cryptographically sound with strong composability properties. More specifically, we define a mapping from a class of cryptographic protocols to Dolev-Yao style symbolic protocols. For this mapping, we show that the symbolic protocol satisfies a certain symbolic criterion if and only if the corresponding cryptographic protocol is UC-secure. We concentrate on mutual authentication and key-exchange protocols that use public-key encryption as their only cryptographic primitive. For mutual authentication, our symbolic criterion is similar to the traditional Dolev-Yao criterion. For key exchange, we demonstrate that the traditional Dolev-Yao style symbolic criterion is insufficient, and formulate an adequate symbolic criterion.

Finally, to demonstrate the viability of the treatment, we use an existing automated verification tool to assert UC security of some prominent key exchange protocols.

[13] J. D. Guttman, F. J. Thayer, J. A. Carlson, J. Herzog, J. D. Ramsdell, and B. T. Sniffen, ``Trust management in strand spaces: A rely-guarantee method,'' in Programming Languages and Systems: 13th European Symposium on Programming (D. Schmidt, ed.), no. 2986 in Lecture Notes in Computer Science, pp. 325-339, Springer, 2004.
[ bib | .ps | .pdf ]
We show how to combine trust management theories with nonce-based cryptographic protocols. The strand space framework for protocol analysis is extended by associating formulas from a trust management logic with the transmit and receive actions of the protocol principals. The formula on a transmission is a guarantee; the sender must ensure that this formula is true before sending the message. The formula on a receive event is an assumption that the recipient may rely on in deducing future guarantee formulas. The strand space framework allows us to prove that a protocol is sound, in the sense that when a principal relies on a formula, another principal has previously guaranteed it. We explain the ideas in reference to a simple new electronic commerce protocol, in which a customer obtains a money order from a bank to pay a merchant to ship some goods.
[14] J. Herzog, Computational Soundness for Standard Assumptions of Formal Cryptography. PhD thesis, Massachusetts Institute of Technology, May 2004.
[ bib | .ps | .pdf ]
The Dolev-Yao model is a useful and well-known framework in which to analyze security protocols. However, it models the messages of the protocol at a very high level and makes extremely strong assumptions about the power of the adversary. The computational model of cryptography, on the other hand, takes a much lower-level view of messages and uses much weaker assumptions. Despite the large differences between these two models, we have been able to show that there exists a relationship between them. Previous results of ours demonstrate that certain kinds of computational cryptography can result in an equivalence of sorts between the formal and computational adversary. Specifically:

  • We gave an interpretation to the messages of the Dolev-Yao model in terms of computational cryptography,
  • We defined a computational security condition, called weak Dolev-Yao non-malleability, that translates the main assumptions of the Dolev-Yao model into the computational setting, and
  • We demonstrated that this condition is satisfied by a standard definition of computational encryption security called plaintext awareness.
In this work, we consider this result and strengthen it in four ways:

  1. Firstly, we propose a stronger definition of Dolev-Yao non-malleability which ensures security against a more adaptive adversary.
  2. Secondly, the definition of plaintext awareness is considered suspect because it relies on a trusted third party called the random oracle. Thus, we show that our new notion of Dolev-Yao non-malleability is satisfied by a weaker and less troublesome definition for computational encryption called chosen-ciphertext security.
  3. Thirdly, we propose a new definition of plaintext-awareness that does not use random oracles, and an implementation. This implementation is conceptually simple, and relies only on general assumptions. Specifically, it can be thought of as a `self-referential' variation on a well-known encryption scheme.
  4. Lastly, we show how the computational soundness of the Dolev-Yao model can be maintained even as it is extended to include new operators. In particular, we show how the Diffie-Hellman key-agreement scheme and the computational Diffie-Hellman assumption can be added to the Dolev-Yao model in a computationally sound way.
[15] J. D. Guttman, J. C. Herzog, J. D. Ramsdell, and B. T. Sniffen, ``Programming cryptographic protocols,'' in Proceedings of the Symposium on Trustworthy Global Computing, April 2005.
[ bib | .pdf ]
Cryptographic protocols are useful for trust engineering in distributed transactions. Transactions require specific degrees of confidentiality and agreement between the principals engaging in it. Moreover, trust management assertions may be attached to protocol actions, constraining the behavior of a principal to be compatible with its own trust policy. We embody these ideas in a cryptographic protocol programming language CPPL at the Dolev-Yao level of abstraction. A strand space semantics for CPPL shaped our compiler development, and allows a protocol designer to prove that a protocol is sound.
[16] J. Herzog, ``A computational interpretation of Dolev-Yao adversaries,'' Theoretical Computer Science, vol. 340, pp. 57-81, June 2005.
[ bib | .ps | .pdf ]
The Dolev-Yao model is a simple and useful framework in which to analyze security protocols, but it assumes that the adversary is extremely limited. We show that it is possible for the results of this model to remain valid even if the adversary is given additional power. In particular, we show that there exist situations in which Dolev-Yao adversary can be viewed as a valid abstraction of all realistic adversaries. We do this in a number of steps:

  1. The Dolev-Yao model places strong assumptions on the adversary. We capture those assumptions in the computational model (an alternate framework with a very powerful adversary) as a non-malleability property of public-key encryption.
  2. We prove an Abadi-Rogaway-style indistinguishability property for the public-key setting. That is, we show that if two Dolev-Yao expressions are indistinguishable to the Dolev-Yao adversary, then their computational interpretations (via a chosen-ciphertext secure encryption scheme) are computationally indistinguishable.
  3. We show that any encryption scheme that satisfies the indistinguishability property also satisfies our (more natural) non-malleability property.
[17] P. Adao, G. Bana, J. Herzog, and A. Scedrov, ``Soundness of formal encryption in the presence of key-cycles,'' in Proceedings of the 10th European Symposium On Research In Computer Security (ESORICS 2005), September 2005.
[ bib | .pdf ]
Both the formal and the computational models of cryptography contain the notion of message equivalence or indistinguishability. An encryption scheme provides soundness for indistinguishability if, when mapping formal messages into the computational model, equivalent formal messages are mapped to indistinguishable computational distributions. Previous soundness results are limited in that they do not apply when key-cycles are present. We demonstrate that an encryption scheme provides soundness in the presence of key-cycles if it satisfies the recently-introduced notion of key-dependent message (KDM) security. We also show that soundness in the presence of key-cycles (and KDM security) neither implies nor is implied by security against chosen ciphertext attack (CCA-2). Therefore, soundness for key-cycles is possible using a new notion of computational security, not possible using previous such notions, and the relationship between the formal and computational models extends beyond chosen-ciphertext security.
[18] R. Canetti and J. Herzog, ``Universally composable symbolic analysis of mutual authentication and key exchange protocols,'' in Proceedings, Theory of Cryptography Conference (TCC), March 2006.
[ bib | .pdf ]
Symbolic analysis of cryptographic protocols is dramatically simpler than full-fledged cryptographic analysis. In particular, it is simple enough to be automated. However, symbolic analysis does not, by itself, provide any cryptographic soundness guarantees. Following recent work on cryptographically sound symbolic analysis, we demonstrate how Dolev-Yao style symbolic analysis can be used to assert the security of cryptographic protocols within the universally composable (UC) security framework. Consequently, our methods enable security analysis that is completely symbolic, and at the same time cryptographically sound with strong composability properties. More specifically, we concentrate on mutual authentication and key-exchange protocols. We restrict attention to protocols that use public-key encryption as their only cryptographic primitive and have a specific restricted format. We define a mapping from such protocols to Dolev-Yao style symbolic protocols, and show that the symbolic protocol satisfies a certain symbolic criterion if and only if the corresponding cryptographic protocol is UC-secure. For mutual authentication, our symbolic criterion is similar to the traditional Dolev-Yao criterion. For key exchange, we demonstrate that the traditional Dolev-Yao style symbolic criterion is insufficient, and formulate an adequate symbolic criterion.

Finally, to demonstrate the viability of our treatment, we use an existing tool to automatically verify whether some prominent key-exchange protocols are UC-secure.


This file has been generated by bibtex2html 1.75

Back to my main page

Last modified: Tue Mar 28 11:09:19 EST 2006