Assignment: Needham-Schroeder Protocol
The purpose of this assignment is to give you experience formalising requirements in the Z notation. The case study is a simplified version of the Needham-Schroeder protocol in which agents send each other encrypted messages, where the messages are encrypted (and decrypted) using keys supplied by a trusted server. The widely used Kerberos computer network authentication protocol is based on the Needham-Schroeder protocol.
Task description
Your task is to complete the missing declarations and predicates in the following partial Z specification of the Needham- Schroeder protocol. A template LaTeX document of this partial specification is available on the Blackboard site. A demonstration of using TeXstudio to produce LaTeX documents, and CZT to type-check Z specifications in LaTeX will be given in the first lecture slot of Week 4.
A pdf file of your completed assignment must be submitted via Blackboard by the due date.
Partial Z specification
Let the given sets
[Message, EncryptedMessage]
denote the set of all possible messages and encrypted messages, respectively. The actual way a message or encrypted message is internally structured is of no concern. Then a key can be thought of as a function that takes an element of type message and converts it into an encrypted message. Hence we can define the set of all keys by
Key == Message → EncryptedMessage
Suppose the agents and server are identified via their names, and we have the given set
[Name]
of all possible names.
The following functions allow us to extract information from messages. For a request message sent to a server, this returns the name of the agent which sent the message, and other returns the name of the agent with which it wants to communicate. For a message with a key, key returns the key, and other returns the agent that can be communicated with using that key.
this : Message → Name key : Message →› Key
other : Message → Name
dom this ∩ dom key = ∅
dom this ∪ dom key = Message
The predicate states that no message is both a request message (in the domain of this) and a key message (in the domain of key). Also, all messages are either request or key messages.
An agent is modelled as having a name, the name of the server (which is not an agent), and a table whose entries map names of other agents and the server to the key used to communicate with them.
Agent
name, serverName : Name
table : Name →
Key
name ƒ= serverName
Initially, the table contains a single key for communication between the agent and the server.
Init
Agent
. . .
An agent may request a key for communication with another agent for which it does not already have a key. This request is sent to the server via a non-encrypted message containing the agent's name and that of the other agent.
RequestKey
An agent may receive a key via an encrypted message from the server and add it to its table. This message also contains the name of the other agent with which the agent can communicate using the received key. A second encrypted message is also received from the server, decrypted and its further encrypted content is sent to the other agent.
ReceiveKeyFromServer
An agent may receive a key via an encrypted message from another agent (but encrypted with the agent's key for communication with the server) and add it to its table. The message also contains the name of the other agent with which the agent can communicate using the received key.
ReceiveKeyFromAgent