Fall 2001, CSE 597E: Quiz 3 and solution - 10 Oct 2001


Please write your Name and Student ID at the top of the page.
  1. [2 point]The non-repudiation property means that (only one answer, please)
    1. A party cannot forbid another party to take part in the protocol
    2. The server cannot refuse the requests of the parties
    3. Proofs of involvement of a party are collected so that he cannot successively deny it
    4. The party cannot refuse to execute a part of the protocol

  2. [2 point] In the trace semantics, A refines B means (only one answer, please)
    1. The traces of A are included in those of B
    2. The traces of B are included in those of A
    3. The traces of A are longer than those of B
    4. The traces of A are shorter than those of B

  3. [2 points] One disadvantage of the trace semantics is that (only one answer, please)
    1. It is not compositional
    2. Traces cannot be used to check temporal properties
    3. Traces represent only the visible actions
    4. The set of traces may be undecidable even for finite-state systems

  4. [2 point] Model checking means (only one answer, please)
    1. To check that a temporal logic formula is valid, i.e. true in all interpretations (LTSs)
    2. To check that a formula has at least one model, i.e. there exists a LTS in which the formula is true.
    3. To check that a formula has no LTS model (proof by contradiction)
    4. To check that a formula is verified by in a given LTS
    LTS here stands for Labeled Transition System.

  5. [2 points] The Casper interface is (only one answer, please)
    1. An interpreter for protocol properties
    2. An interpreter for security protocols
    3. A compiler from protocols descriptions to CSP
    4. An interactive tool for testing protocols properties

  6. [Bonus question, points 5] Consider the Zhou-Gollmann protocol describer at page 19 of previous lecture notes. Assume that we switch the second and the third step of the protocol. What can we say about the properties of the protocol?
    1. They are maintained
    2. We lose non-repudiation of origin
    3. We lose non-repudiation of recipient
    4. We lose both
    Please motivate your answer.

    Motivation:It the second and the third step of the protocol are exchanged, then an evil recipient has the possibility of getting the encrypted message from the sender, and the key to decode it from the server, without sending any message FNRR to the sender. Hence the sender will have no evidence that the recipient received the encrypted message.