++++++++++++++++++ FME2001: - Review reports for paper 59 +++++++++++++++++++++ - Dear author(s) : this file was extracted automatically from a very large - mailbox. In case you find any problem concerning mail encodings (or any - other kind of anomaly disturbing your understanding of the reviews) please - email any of the PC cochairs (pamela@research.att.com,jno@di.uminho.pt). ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ PAPER NUMBER: 59 CATEGORY: 2 TITLE: Secrecy-preserving Refinement AUTHOR(S): Jan Jürjens -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper proposes a formulation of a security property, secrecy, within the specification framework FOCUS. This property is (unusually) preserved by refinement and thus appropriate for use in stepwise development. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 2.5 Please comment your rating: This paper is quite theoretical and not mainstream formal methods. However, the application of formal methods to security is of increasing interest and will be relevant to the conference. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 4 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 5 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: The novelty is in the specification and description of security protocols and properties in a way that is preserved by refinement; and in the use of FOCUS to do this. 6. How WORTHWILE is the goal of the authors? Comment: Very worthwhile. Security properties are difficult to express or work with in a useful and practical way. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Very well - the motivation is clear (that this formulation enables stepwise refinement) and its benefits are well-understood. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Yes 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: The work at this stage is primarily theoretical. It is clearly applicable though it is not at that stage yet - doing security proofs is still at quite an early stage. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The paper is well-written, clear, and easy to understand. It would benefit from a description of how the TLS flaw was found. It shuold be clearer whether this flaw is in the real TLS, or whether the variant studied in this paper is not the real thing. 11. Were there any formatting or mechanical problems with this paper?: no Are the figures and length acceptable?: yes Are the references correct?: yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: The early justification/motivation is given as the fact that non-interference is not (in general) preserved by refinement. Some further motivation is required with regard to secrecy, which is the property you are concerned with. In particular, an example on page 3 (penultimate paragraph) to illustrate the point about the fine grained model would be helpful. On page 2, could you say how your approach addresses the examples in [CJ95, RS98] etc, which exploit features of the implementations of cryptographic mechanisms. This is not clear in the paper. The figure on page 12 needs longer arrows - the text overruns them. You may also want to look at Sewell's work (see CSFW 1999, 2000) characterising information flow, which seems to bear some relationship to your secrecy property. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 59 CATEGORY: 2 TITLE: Secrecy-preserving Refinement AUTHOR(S): Jan Jürjens -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): Security properties, often defined in terms of sets of traces, are often not preserved by trace inclusion refinement. This paper gives a notion of secrecy that *is* preserved. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 2 Please comment your rating: 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 4 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 2 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: Refinement preserving secrecy, presumably. 6. How WORTHWILE is the goal of the authors? Comment: Quite. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Reasonably well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: I have no idea at all. The notation is so mind-boggling that I did not manage to get through the technical parts of this paper. This is mainly due to symbol overloading: I finally figured out that subscripting meant indexing of streams, except for the many cases where it doesn't. For example, subscripting with lower case d and e is indeed indexing, but with lower case c it is suddenly about closed processes. I still don't know what p_d at the bottom of page 8 is supposed to be. Similarly, {} means both set formation and encryption, both of which used in the last line of page 8. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: OK 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Well-written for those who are already intimately familiar with the formalism. 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Yes Are the references correct?: Yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 59 CATEGORY: 2 TITLE: Secrecy-preserving Refinement AUTHOR(S): Jan Jürjens -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper tackles development by refinement of things related to cryptography. There are some delicate (compositionality) questions addressed (cf. "refinement paradox"). The general framework is that of (Broy/Stoellen) stream assertions; specifically, a rely/guarantee-approach is adopted. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 2 (but that's a shame - maybe this is an area FME should get more involved in?) Please comment your rating: I did :-) 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 4 NB: There should be a correlation between the two rates above. Well, it doesn't - I think the paper is good (modulo comments below) Of course, if you have masses of superb stuff on Z logics, this might get squeezed out. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 3 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: I've played with rely/guarantee for hiding info (especially key distribution) but this is a serious piece of research. 6. How WORTHWILE is the goal of the authors? Comment: Very! 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: I find the paper very dense - hard work - but I can't suggest ways to significantly simplify the presentation 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: As far as I can judge 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: Fine! 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The section of "Related work" adds little (unless one has read all of the references) Maybe earlier use of some well-chosen examples could help without increasing the length by much. 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Yes Are the references correct?: As far as I can see 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: You could add references to Rely/Guarantee work (or is it all in the (forthcoming) book?) +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++