CMU 15-827 |
Security and Cryptography |
Fall 1998 |
Authentication |
||
Wing |
Homework 2 |
Due: 12 October 1998 |
Consider the following scenario: Alice wants to login on a computer system. In order to gain access she has to communicate her password to the system. Unfortunately the keyboard (and the cable connection between the keyboard and the system) cannot be trusted since there may be a passive adversary recording the key strokes or tapping the line.
Conversely, let us assume that the display used by Alice (and the connection between the system and the display) is secure, meaning it cannot be monitored by an adversary.
Devise a password protocol that will allow Alice to access the system without disclosing her keys to the adversary.
Choose three principles given by Needham and Abadi in their guidelines for designing cryptographic protocols paper. For each, give an example where their principle applies and results in an improved protocol, and an example where their principle leads to a poorer protocol.
Suppose I want to leak information out of a secure facility (for example, the secret plans for Intel’s new processor). Pick one of the authentication protocols we discussed in class and describe how I can deliberately leak information using this protocol.
You want to synchronize computers to the real time. One solution is to buy a WWV receiver or a GPS receiver. What are the security threats with this approach? (The relevant information about WWV and GPS receivers is just the existence of a time signal.)
Devise a secure way to synchronize real time at minimum cost and minimum human intervention.
In this problem you will apply a slight modification of the BAN Logic to the concrete STS protocol discussed in Lecture 2. Assume p is a large prime, g is a generator modulo p and all operations are performed modulo p.
Assume the BAN Logic with the following modifications:
P believes DH(P, g^{x}), P believes DH(Q, g^{y})
P believes P ^{K} Q
where K = g^{xy}
P believes ^{PK} Q, P sees {x}_{PK}^{-1}
P believes x
Now here is a description of the idealized STS protocol you are going to work with (here K = g^{xy}):
We want to prove that
A believes A ^{K } B (Goal 1)
and
B believes A ^{K} B (Goal 2)
starting with the following assumptions:
A believes fresh(g^{x}) B believes fresh(g^{y})
A believes DH(A, g^{x}) B believes DH(B, g^{y})
A believes ^{PB } B B believes ^{PA} A
To show a correspondence between different models of authentication protocols, give an encoding of the Dolev-Yao algebraic model of computation for name-stamp protocols (Section III of their paper) in terms of the Abadi-Tuttle state-machine model of computation (Section 5 of their paper).
Back to Lectures
Heather L. Marko
Last Modified: September 1998