PAPER NUMBER: 	14
PAPER TITLE: 	Using SPIN to Model Cryptographic Protocols
AUTHORS:	Li Yongjian, Xue rui 

Score values              0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). 
-------(Review 1)-----------------------------------------------------------------------------------------------------------
Appropriateness:  	4
Originality: 	3
Technical strength: 	4
Presentation: 	2
-------------------------------------------------------------------------------------------------------------------
Overall: 		4


Comments to the authors: 
1. I'd like to see authors discuss more fully on the completeness of deduction rules of an intruder.
2. I'd like to see fully discussion on the scope and limitation of the applicability of the technique. Which attacks can and can't be analyzed?
3. Please revise discussion on Promela encoding to avoid redundancy and places where discussions are sketchy.



Score values    3          0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). 
--------(Review 2)----------------------------------------------------------------------------------------------------------
Appropriateness: 4
Originality: 3
Technical strength: 3
Presentation: 2
-------------------------------------------------------------------------------------------------------------------
Overall: 

  Summary:
  This paper describe a general method (in macros) to 
  model Cryptographic Protocols in SPIN which is not
  designed to handle many features of Cryptographic Protocols.

  Comments:


Comments to the authors: 


Score values              0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). 
----------(Review 3)--------------------------------------------------------------------------------------------------------
Appropriateness: 3
Originality: 3
Technical strength: 2
Presentation: 2
-------------------------------------------------------------------------------------------------------------------
Overall: 3

Comments to the authors: 

This paper deals with the very interesting 
research topic.
Judging from the presented examples, 
the proposed modeling method seems sound.
However, I wonder if the proposed technique
is general, since only some examples of the 
model construction are given.
It would be better if a formal definition
of the cryptographic protocol is given
and a general model construction algorithm 
is presented.