Cryptographic Protocol Specification and Analysis

We propose Rewriting logic as an executable specification formalism for security protocols that offers some novel advantages. The level of specification is detailed enough to capture essential operational aspects and to allow rapid prototyping and debugging by directly executing the specifications.

A message-passing object-oriented approach seems particularly natural for communication protocols and can be naturally formalized in rewriting logic. This is illustrated by using the Needham-Schroeder Public-Key protocol (NSPK) as a running example. Using the rewriting logic-based Maude interpreter, we can prototype and debug the NSPK protocol specification. But since a protocol can have many different behaviors, to properly analyze the system it becomes important to explore not just the single execution provided by some default strategy, but many other executions. For this purpose we defined a bounded depth-first search strategy that explores all executions of a system for a given initial configuration searching for attack situation.
 

The NSPK Protocol is a cryptographic protocol for the authentication of pairs of agents in a distributed computer system. For instance, agents want to be assured of each other's identity before they exchange security-critical data. Thus, an intruder should not be allowed to impersonate another agent. For this purpose, initiator and responder of a communication mutually authenticate each other. NSPK uses public key cryptography, i.e., each agent possesses a public key which can be accessed by all agents and a secret key, which is the inverse of the public key. Moreover, nonces are used in the protocol. Nonces are freshly generated, random numbers to be used in a single run of the protocol. It is assumed that these numbers are generated in such a way that they cannot be guessed by other agents. A textbook-style simplified description of NSPK is:

Message 1: A -> B: A.B.{Na,A}PK(B)

Message 2: B -> A: B.A.{Na.Nb}PK(A)

Message 3: A -> B: A.B.{Nb}PK(B)

In this protocol A tries to establish a communication with B. Thus, A plays the role of the in Aitiator and B reacts in the responder role. A encrypts his nonce Na with the public key of B and sends it along with his identity to B. Now A is in a waiting status. B decrypts the message, creates a new nonce and sends back to A the concatenation of both nonces encrypted with the public key of A. After this, B is waiting for the answer from A. A can decrypt the message sent by B. In case the contents of the message is the concatenation of his own nonce Na plus another nonce, A can be assured that the message was sent by B, because B is the only agent who can decrypt the message sent by A containing the nonce Na. Thus, A establishes a communication with B. Moreover, to acknowledge to B the receipt of B's nonce, A separates it from the message and sends it back. If B receives this message from A, he can be assured of being talking to A and, therefore, of having established a communication with A.

As one can see, there is a lot of implicit knowledge in the textbook-style specification of the NSPK Protocol. Moreover, there are open questions concerning how agents behave if they receive a message which does not have the expected contents, e.g., if A receives a message from B which does not contain his nonce. Our intention is to make this implicit knowledge explicit and to clarify fuzzy parts of the description by formalizing the protocol in rewriting logic. In addition to the protocol requirements given above, we will provide a Maude specification which allows multiple sessions for an agent. For instance, an agent may simultaneously participate in several runs of the protocol. In this way, an agent may simultaneously play different roles (e.g., initiator or responder) in different runs.
 
 

Maude Specifications and Samples

NSPK specification and search strategy

Sample runs and search scenarios
 
 

Papers

[Maude Home Page]