Assignment 1 - Verifying properties with SPIN

Part 1 - The dining philosophers

This assignment is about modeling the dining philosophers problem in Promela. A number of philosophers have gathered around a table to eat spaghetti. There are N philosophers around the table and N forks on the table. Philosophers are a very special breed and they need two forks to be able to eat. This means that they need to share forks with each other. When a philosopher is not eating he likes to busy himself with some thinking. The picture to the left illustrates five philosophers sitting around a table with five forks.

proctype phil(int id) {
  do
  ::/* ... */
  od
}

proctype phil(int id) {
do 
  ::printf("thinking\n");
    /* ... */
    printf("eating\n");
    /* ... */
od
}

#define NUM_PHIL 4

proctype phil(int id) {
do 
  ::printf("thinking\n");
  /* ... */
  printf("eating\n");
  /* ... */
od
}

init {
int i = 0; 

do 
:: i >= NUM_PHIL -> break
:: else -> run phil(i); 
           i++ 
od 
}

$ spin Lab1_1.pml 

thinking
     eating
     thinking
         thinking
         eating
             thinking
     eating
             eating
         thinking
         eating
             thinking
             eating
     thinking
         thinking
     eating
         eating
                 thinking
     thinking
                 eating
             thinking
         thinking
             eating
     eating
         eating
     thinking
             thinking
                 thinking
     eating
         thinking
                     thinking

                      Philosopher 3 is thinking
          Philosopher 0 is thinking
              Philosopher 1 is thinking
                  Philosopher 2 is thinking
              Philosopher 1 is eating with forks 1 and 0
                  Philosopher 2 is eating with forks 2 and 1
              Philosopher 1 is thinking
                  Philosopher 2 is thinking
                      Philosopher 3 is eating with forks 3 and 2
              Philosopher 1 is eating with forks 1 and 0
                      Philosopher 3 is thinking
              Philosopher 1 is thinking
                  Philosopher 2 is eating with forks 2 and 1
                      Philosopher 3 is eating with forks 3 and 2

1. Use assertions in your code to verify this property about forks.
2. 1. Does your model has deadlocks? If yes, use SPIN to derive a counter example showing a problematic trace. Modify your solution to eliminate deadlocks.
   2. Verify absence of deadlocks in your model using SPIN.
3. Verify property (1) with an LTL formula instead of assertions.

Reporting

1. A file Dining.pml which is your Promela model for the Dining Philosophers problem.
2. A text report named Report_Dining.txt describing your solution to (1) - (3) including all relevant information on how to use your model.
3. Other supporting files, such as SPIN-generated (.trail) for the counterexamples that you discuss in your report.

Part 2 - Needham-Schroeder protocol verification

Background - security protocols

Most communication on the Internet and other networks is, as you may know, publically visible to anyone listening in. In some situations it is preferable to have a secret communication channel, for example when visiting the website of your bank or when sending your password to login to Facebook. One way to do this is by using public key cryptography. Here each principal X involved in the network has published a public key pX while keeping hidden from everybody else a corresponding secret key sX. Communication to X can now be encrypted under this public key pX and can only be decrypted using sX, i.e. the key only in possession by X.

This is not an entire solution to the problem though. Performing encryption and decryption under public key cryptography is computationally rather expensive. To establish a faster communication channel one can use symmetric key cryptography. Here a pair of principals shares the same key, which gives faster encryption and decryption (somehow, for details you have to take a course in cryptography). This however has the problem that in a network with n principals, there must be n(n-1) unique shared keys - which can mean a rather large number - and is therefore also not perfect.

One goal of security protocols is to get the best of both worlds. Using public key cryptography, two principals communicate two random numbers. If all steps in the protocol are executed correctly, it should be the case that

1. Each principal has proven to be the person he claims to be (authenticity)
2. The involved principals, and only they, know the communicated random numbers (confidentiality)

The communicated random numbers can now be somehow used to construct a symmetric (shared) key and, since no one else knows these numbers, further communication can be encrypted under this shared key.

Needham-Schroeder protocol

In this assignment we have a look at a famous security protocol, the Needham-Schroeder protocol. It is well-known for being vulnerable to an attack on both confidentiality and authenticity, and in this assignment we aim to find this attack using model checking. The protocol is as follows:

where

That is, X sends to Y a message consisting of X's identity and a nonce encrypted under Y's public key. Y's reply consists of X's nonce, proving that Y is the owner of the secret key, and Y's nonce, encrypted under X's public key. The nonces should now only be known to both principals, and can be used to construct a shared symmetric key (confidentiality). Finally, X sends back Y's nonce, to prove that he has the right secret key (authenticity).

Modelling the network:

Agents. We start with two agents: Alice, and Bob and consider a run of this protocol between them in isolation (with no other principals). We assume the existence of public keys kA for Alice, and kB for Bob. The code below is a PROMELA model for Alice. It also contains supporting declarations for modelling encryption and the network.

Nonces. In a real system the nonces used in the actual protocol would be random numbers generated by their respective agent and used only once for the purpose to establish a common secret between two agents. Here,to keep the model simple and the state space small, nonces are modelled as precomputed names nonceA and nonceB. But initially agent A knows still only nonceA and agent B knows only nonceB. Any other agent, in particular the intruder, does not know any nonces a priori. Nonces may only be learned by receiving/intercepting messages containing the nonces and being able to decrypt these messages. Keep this in mind when modeling the intruder.

Messages. To represent encrypted messages we use a record Crypt that contains three entries: a key and two data entries (dubbed content1 and content2). With such representation encryption is modelled as creating a variable of type Crypt, where the key is the public key of the receiver. Therefore, decryption can only be done by matching the key entry with the key in posession of the agent.

Network. The network is modelled as a single message channel shared by all agents on the network. For simplicity, we use synchronous communication on the network, which is indicated by a buffer length of 0. While this does not affect the possible communication patterns, it helps to reduce the size of the model. A message on the network is a triple consisting of an identification tag (the message number), the intended receiver, and an "encrypted" message body.

Verification aids. For verification purposes we also introduce global variables partnerA, partnerB, statusA, statusB (ghost variables). The variable partnerA specifies who is Alice's intended partner. Similarly, partnerB indicates who is Bob's partner. In the beginning we explicitly set partnerA = agentB.

mtype = {ok, err, msg1, msg2, msg3, keyA, keyB, agentA, agentB,
         nonceA, nonceB };

typedef Crypt { mtype key, content1, content2 };

chan network = [0] of {mtype, /* msg# */
                       mtype, /* receiver */
                       Crypt
};

/* global variables for verification*/
mtype partnerA, partnerB;
mtype statusA = err;
mtype statusB = err; 

/* Agent (A)lice */
active proctype Alice() {
  /* local variables */
  
  mtype pkey;      /* the other agent's public key                 */
  mtype pnonce;    /* nonce that we receive from the other agent   */
  Crypt messageAB; /* our encrypted message to the other party     */
  Crypt data;      /* received encrypted message                   */


  /* Initialization  */
  
  partnerA = agentB;
  pkey     = keyB; 

  /* Prepare the first message */
  
  messageAB.key = pkey;
  messageAB.content1 = agentA;
  messageAB.content2 = nonceA;  

  /* Send the first message to the other party */
  
  network ! msg1 (partnerA, messageAB);

  /* Wait for an answer. Observe the we are pattern-matching on the
     messages that start with msg2 and agentA, that is, we block until 
     we see a message with values msg2 and agentA as the first and second  
     components. The third component is copied to the variable data. */

  network ? (msg2, agentA, data);

  /* We proceed only if the key field of the data matches keyA and the
     received nonce is the one that we have sent earlier; block
     otherwise.  */

  (data.key == keyA) && (data.content1 == nonceA);

  /* Obtain Bob's nonce */
  
  pnonce = data.content2;

  /* Prepare the last message */  
  messageAB.key = pkey;
  messageAB.content1 = pnonce; 
  messageAB.content2 = 0;  /* content2 is not used in the last message,
                              just set it to 0 */

  
  /* Send the prepared messaage */
  network ! msg3 (partnerA, messageAB);

  
  /* and last - update the auxilary status variable */
  statusA = ok;
}

active proctype Bob() {
   printf("placeholder for Bob\n")
}

Task 1: Write a model for Bob.

Write a model for Bob that communicates with Alice's. In the official protocol, the principal identifier in the first message (X) is used by Bob to determine with who he is communication, but we simplify this to Bob always assuming it is Alice who initalizes communication. Hence we always have:

partnerB = agentA;
pkey     = keyA;

Run the simulation with your implementation of Bob. As a last command in your model for Bob add a statement

statusB = ok;

Task 2: SPIN

In this simple two-agent world everything should run smoothly and both Alice and Bob should always be able to reach the last statements in their corresponding models. In fact, this can be verified this with a Temporal Logic formula saying that eventually we reach a state where both statusA and statusB are ok.

Verify this property with a Temporal Logic formula in SPIN.

Task 3: Introducing the attacker.

To study security guarantees of our protocol we investigate how communication between Alice and Bob is affected in the presence of a third agent: Intruder. The listing below presents an intruder (also referred as attacker) process.

First, we extend declarations of possible agents, keys, nonces and agents to include the one for the attacker.

mtype = {... , agentI, keyI, nonceI } 

The code for the intruder then looks as follows:

active proctype Intruder() {
  mtype msg, recpt;
  Crypt data, intercepted;
  do
    :: network ? (msg, _, data) ->
       if /* perhaps store the message */
         :: intercepted.key   = data.key;
            intercepted.content1 = data.content1;
            intercepted.content2 = data.content2;
         :: skip;
       fi ;

    :: /* Replay or send a message */
       if /* choose message type */
         :: msg = msg1;
         :: msg = msg2;
         :: msg = msg3;
       fi ;
       if /* choose a recepient */
         :: recpt = agentA;
         :: recpt = agentB;
       fi ;
       if /* replay intercepted message or assemble it */
         :: data.key    = intercepted.key;
            data.content1  = intercepted.content1;
            data.content2  = intercepted.content2;
         :: if /* assemble content1 */
              :: data.content1 = agentA;
              :: data.content1 = agentB;
              :: data.content1 = agentI;
              :: data.content1 = nonceI;
            fi ;     
            if /* assemble key */
              :: data.key = keyA;
              :: data.key = keyB;
              :: data.key = keyI;
            fi ;
            data.content2 = nonceI;
       fi ;
      network ! msg (recpt, data);
  od 
}

This process is very nondeterministic in the choice of its actions and their sequence. Still, the current attacker is very limited: it picks up messages from the network, replays some messages, or initiates a new run with one of the protocol.

Disclaimer: This is approach is not, in general, the best way to perform verification of security protocols. Modelling the attacker as a process allows for mistakes in the intruder's capabilities, making the attacker either too powerful or too weak. In this assignment we focus on using SPIN and modelling properties with Promela and LTL, but if you are interested in verifying protocols in particular a tool like ProVerif is more recommended.

Add the above code to your model and simulate it. You may notice that with the introduction of the attacker principal the property from Task 2 becomes too strong and is no more true. Find a counterexample with SPIN and explain what exactly causes it to fail.

Task 4: New assumptions on the attacker.

In the above model the intruder is a complete outsider. In this task we strengthen assumptions about the intruder. Not only can our attacker intercept and replay messages, but now he can also be a valid recipient of messages from Alice, that is, Alice may decide to start a communication with the intruder. Effectively, this corresponds to the intruder being a legitimate user of a system - an insider with malicious intentions.

Start with modifying the code for Alice, so that she nondeterministically chooses either Bob or Intruder as her communication partner for her run of the protocol. The result of this choice should be reflected in the variable partnerA. Once this choice is made the subsequent protocol messages should be encrypted with the key of the corresponding principal, that is, with keyB when partnerA is agentB, and with keyI when partnerA is agentI - Bob still assumes he is always contacted by Alice.

Task 5: Extending the Intruder.

Now that the intruder may receive messages encrypted with his key, he should be able to decrypt and access the content of those messages. Extend the intruder process to reflect this. Add two more ghost global variables that represent the attacker's knowledge of the nonces:

/* global variables for verification*/
...
bool knows_nonceA, knows_nonceB;

Initialize these variables to false. In your modified code for the intruder, you will have to set these variables to true only when successful decryption of an intercepted message yields nonceA or nonceB. To add possibility of decryption extend the intruder with another if block which checks the key of the intercepted data. If the key matches with the one of the intruder, proceed to check the content; skip otherwise.

Task 6: Attack

At this step your implementation should be ready to analyze security guarantees of our protocol. The following three properties specify the properties of the protocol:

1. If both Alice and Bob reach the end of their runs (i.e. both statusA and statusB are ok) then Alice's communication partner is Bob, and Bob's communication partner is Alice. 

2. If agent A reaches the end of its run (statusA is ok) and it believes it is talking to B  (partnerA  is agentB) then the intruder does not know A's nonce (!knows_nonceA)

3. Similarly for B's nonce. That is: if agent B reaches the end of its run (statusB is ok) and it believes it is talking to A  (partnerB  is agentA) then the intruder does not know B's nonce (!knows_nonceB)

Encode the above properties as Temporal Logic formulas and use SPIN to verify them. Since the protocol that we have presented is buggy, you should be able to find a counterexample to these properties.

Which of the properties (1) - (3) is violated? Can you explain in your words what happens in your counterexample?

Task 7: Patching the protocol

There is a well-known patch to the protocol: in the patched version the second message of the protocol

is replaced with a message that contains the identity of principal Y:

Modify your model to implement this patch. Re-verify that your new model satisfies properties (1)-(3) from Task 6.

Reporting

For Part 2 of the assignment we expect:

1. A series of files
   1. NS2.pml (for the model that you verify in Task 2) and a file named BOTH_ARE_OK.PRP with the negated form of the LTL formula in one line,
   2. NS3.pml (for the model in Task 3)
   3. NS6.pml (for the model that you verify in Task 6), and one file for each property to be verified named PROP_AB.PRP, PROP_A.PRP, PROP_B.PRP containing the negated form of the LTL formula expressing the property
   4. and NS7.pml (for your final correct model)
2. A text report named Report.txt describing your solution to Tasks 1-7 and information on how you did the verification.
3. Other supporting files, such as SPIN-generated (.trail) for the counterexamples that you discuss in your report.

Reporting

• See respective sections of Part 1 and Part 2.
• Please submit the report in plain text format (.txt). Avoid other formats as this may cause delays in grading your submission.
• Submit via Fire

Tips

• If you find SPIN running out of memory try using -DCOLLAPSE option for compiling your verifier.
• For verifying liveness properties add -DNOREDUCE as a flag to gcc
• If you want to you can break down Temporal Logic formulas using the #define syntax.

Testing

• You can use this script to help you test your Promela files in a compact way.
• It requires Haskell, any version newer than 7.0.2 (it could work on an older one, but we didn't test that).
• The first argument is the path to the directory where you have your properties and Promela files (it is assumed that they are all in the same directory).
• The second argument is the name of a file where you specify for each of the 4 properties(in the order they are mentioned in the lab) whether they are liveness or safety properties. So basically you need a file with 4 lines where each line is either safety or liveness. In this way, the right set of commands will be chosen to test each property
• After running the testing tool, you will get a short log, telling you which properties are verified by Spin and which aren't.

References

• Spin reference card (PDF)