[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 |

[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. |

[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. |

[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. |

[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. |

[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. |

[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 |

[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 |

[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: |

[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 |

[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. |

*This file has been generated by
bibtex2html 1.75*

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