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

The main objectives of the second part of the assignment is to find an attack on a security protocol using model checker. For this assignment we will use Needham-Schroeder protocol public key protocol (you do not need to have preliminarily knowledge about the protocol). The goal of the protocol is to establish a shared key between the two principals.

The protocol runs between two principals X and Y, and consists of three messages:

1. X -> Y: {X, NX}_{kY}
2. Y -> X: {NX, NY}_{kX}
3. X -> Y: {NY}_{kY}
   

In the above description X -> Y: M means that agent X sends message M to agent Y. Notation {content}_{kP} stands for encrypting content with the public key kP. The shared secret established by the end of this protocol is a composite of two secrets NX, and NY (called nonces), where NX is produced by agent X, and NY is produced by agent Y.

Modelling the network:

We start with two agents: Alice, and Bob and consider a run of this protocol between them in isolation. We assume 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 network.

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.

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  and decryption is done by checking the key entry for the matching key.

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.

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. Run the simulation with your implementation of Bob. As a last command in your model for Bob add a statement

statusB = ok;

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.

Task 2: SPIN

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.

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.

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 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

Y -> X: {NX, NY}_{kX}

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

Y -> X: {Y, NX, NY}_{kX}

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

Hints

Translating LTL formulas to never claims does not always work as expected with SPIN. In particular, the implication symbol -> causes mistcal error messages with SPIN. The solution is not to use an implication, but an equivalent formula that only uses negation and disjunction. So instead of:

you should use:

Moreover, the equivalence operator <-> will not work either, but using it in the Lab should not be necessary. However, if you feel it is necessary then:

should do the trick.

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.
• Important:
  1. You need to login into remote11.chalmers.se or remote12.chalmers.se. If for some reason you cannot access any of the two machines, please contact one from the SEFM team.
  2. Download the archive sanityTest.zip
  3. Extract the archive.
  4. You should now see a directory named sanityTest.
  5. Change into this directory cd sanityTest.
  6. Inside this directory you have one directory called Lab1. Copy all your solution files named as requested in the assignments into the directory Lab1.
  7. Make sure that you are now in the directory sanityTest again.
  8. Execute then ./Check.
  9. If you get the message that no problems have been found with your solution, then proceed with the next step. Otherwise please fix your solution first before submitting it. If you encounter problems at this step and you suspect it might be a problem with the checking program itself, please contact the course assistants in time.
  10. 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
• For encoding Temporal Logic formulas you may use #define syntax.

References

• Spin reference card (PDF)