#define NONCE_MAX 8
#define KEY_MAX 8
#define STORE_MAX 10

mtype {msg1, msg2, msg3};
byte used_nonce = 1, used_key = 1, s_ptr;

typedef Crypt {
  byte key;
  byte info1;
  byte info2;
};

typedef stored_data {
  mtype msg_type;
  Crypt data;
}
stored_data stored_mesg[STORE_MAX];

typedef channel {
  chan C = [0] of { mtype,  /* message type */
                    bool,   /* is it sent by intruder?  */
                    Crypt };
};
channel proc_chan[KEY_MAX];                                

bool known_nonce[NONCE_MAX], known_key[KEY_MAX];
bool nonce_introduced[NONCE_MAX];

bool flaw;  /* security property */

/* nondeterministically chooses a known nonce */
inline chooseNonce(nonce) {
  nonce = 1;
  do  
    :: (known_nonce[nonce] == true) ->
       break;   
    :: nonce++;
       if 
         :: (nonce >= NONCE_MAX) -> 
            nonce = 1; /* to ensure nonce has a sensible value */
            break;
         :: else -> skip;
       fi;
  od;
}

/* nondeterministically chooses a running process */
inline getAValidProcess(i) {
  i = 1;
  do  /* choose the process to send the message */
    :: break;
    :: i++;
       if
         :: (i == KEY_MAX - 1) ->
            break;
         :: else -> skip;
       fi;
  od;
}

inline modifyFlawStatus(k) {
  if
    :: (nonce_introduced[k] == true) ->
       flaw = true;
    :: else -> skip;
  fi;
}

inline replayMessage() {
  i = 0;
  do
    :: (i > s_ptr) -> break;
    :: else -> 
       if
         :: (1) ->
            msg = stored_mesg[i].msg_type;
            data.key = stored_mesg[i].data.key;
            data.info1 = stored_mesg[i].data.info1;
            data.info2 = stored_mesg[i].data.info2;
            
            getAValidProcess(i);
            
            proc_chan[i].C!msg(true, data);
            break;
         :: skip;       
       fi;
       i++;
  od;   
}


init {

  byte j;

  run procI(1);
  run procA(2);
  run procB(3);
  
  j = 3;
  do  /* create processes nondeterministically */
    :: break;
    :: j++;
       if
         :: (j >= KEY_MAX) ->
            break;
         :: else ->
            if
              :: run procA(j);
              :: run procB(j);
            fi;
       fi;
  od;
  
}

proctype procA(int agent_id) {
  
  byte my_nonce, recvd_nonce;
  byte i = 1;
  chan my_chan = proc_chan[_pid].C;
  chan p_chan;
  Crypt data;
  
  atomic {
    
    getAValidProcess(i);  /* choose the partner */
    
    p_chan = proc_chan[i].C;
    used_nonce++;
    my_nonce = used_nonce;
    data.key = i; data.info1 = _pid; data.info2 = my_nonce;
    p_chan!msg1(false, data); /* 0 to signify that it is not sent by intruder proc */
  }

  my_chan?msg2(_, data);
  
  do  /* if unexpected message go to infinite loop */
    :: ((data.key == _pid) && (data.info1 == my_nonce)) -> break;
  od;
  
  atomic {
    recvd_nonce = data.info2;
    nonce_introduced[recvd_nonce] = true;
    data.key = i; data.info1 = recvd_nonce; 
    p_chan!msg3(false, data);
  }     
  
}

/* Process B */
proctype procB(int agent_id) {
  
  byte partner, p_nonce, my_nonce;
  chan my_chan = proc_chan[_pid].C;
  chan p_chan;
  Crypt data;
  
  my_chan?msg1(_, data);
  do /* if unexpected message go to infinite loop */
    :: (data.key == _pid) -> break;
  od;
  
  atomic {
    partner = data.info1; p_nonce = data.info2;
    nonce_introduced[p_nonce] = true;
    p_chan = proc_chan[partner].C; 
    used_nonce++;
    my_nonce = used_nonce;
    data.key = partner; data.info1 = p_nonce; data.info2 = my_nonce;
    p_chan!msg2(false, data);
  }
  

  my_chan?msg3(_, data);
  do /* if unexpected message go to infinite loop */
    :: ((data.key == _pid) && (data.info1 == my_nonce)) -> break;
  od;   
}

/* Intruder Process */
proctype procI(int agent_id) {
  
  mtype msg;
  chan temp_chan;
  Crypt data;
  byte i, j, k, nonce;
  
  atomic {
    known_nonce[1] = true; /* nonce 1 is for the intruder */
    known_key[1] = true;
  }
  
  do 
    ::  /* intercept a message */
       if  /* choose a channel to intercept */
         :: proc_chan[1].C?msg(false, data);
         :: proc_chan[2].C?msg(false, data);
         :: proc_chan[3].C?msg(false, data);
         :: proc_chan[4].C?msg(false, data);
         :: proc_chan[5].C?msg(false, data);
         :: proc_chan[6].C?msg(false, data);
         :: proc_chan[7].C?msg(false, data);
       fi;
       atomic {
         if
           :: (s_ptr < STORE_MAX) ->
              stored_mesg[s_ptr].msg_type = msg;
              stored_mesg[s_ptr].data.key = data.key;
              stored_mesg[s_ptr].data.info1 = data.info1;
              stored_mesg[s_ptr].data.info2 = data.info2;
              s_ptr++;
           :: else -> skip;     
         fi;
         
         if
           :: (msg == msg1) ->
              j = data.info1; k = data.info2;
              
              if /* if possible decrypt */
                :: (known_key[data.key]) ->
                   if          
                     :: (!known_nonce[k]) -> modifyFlawStatus(k);
                     :: else -> skip;
                   fi;
                   known_nonce[k] = true;
                   
                :: else -> skip;
                           nonce_introduced[k] = true;
              fi;
              
           :: (msg == msg2) ->
              j = data.info1; k = data.info2;
              
              if /* if possible decrypt */
                :: (known_key[data.key]) ->     
                   
                   if 
                     :: (!known_nonce[j]) -> 
                        modifyFlawStatus(i, j);
                     :: else -> skip;
                   fi;
                   known_nonce[j] = true;
                   
                   if 
                     :: (!known_nonce[k]) ->
                        modifyFlawStatus(i, k);
                        
                     :: else -> skip;
                   fi;
                   known_nonce[k] = true;
                   
                :: else -> skip;

                           nonce_introduced[j] = true;
                           nonce_introduced[k] = true;
              fi;
              
           :: (msg == msg3) ->
              j = data.info1;
              
              if                                 /* if possible decrypt */
                :: (known_key[data.key]) ->

                   if 
                     :: (!known_nonce[j]) ->
                        modifyFlawStatus(i, j);
                        
                     :: else -> skip;
                   fi;
                   known_nonce[j] = true;
                   
                :: else -> skip;
                           nonce_introduced[j] = true;
                           
              fi;
              
           :: else -> skip;
         fi;

       }
    ::      /* message replay */
       atomic { replayMessage() };
       
    :: atomic { /* synthesize a message */

      getAValidProcess(i); /* choose the process to send the message */
      temp_chan = proc_chan[i].C; data.key = i; 
      
      if
        :: /* create a message of type 1 */ 
           chooseNonce(nonce);   /* choose the nonce for 1st field */
           getAValidProcess(i);  /* choose the initiator */
           data.info1 = i; data.info2 = nonce;
           temp_chan!msg1(true, data);
           
        :: /* create a message of type 2 */
           chooseNonce(nonce);   /* choose the nonce for 1st field */
           data.info1 = nonce;
           chooseNonce(nonce);   /* choose the nonce for 2nd field */
           data.info2 = nonce;
           temp_chan!msg2(true, data);
           
        :: /* create a message of type 3 */
           chooseNonce(nonce);   /* choose the nonce for 1st field */
           data.info1 = nonce;
           temp_chan!msg3(true, data);
      fi;
    }
       
  od;
}

never { /* !([](!flaw)) */
T0_init:
  if
    :: ((flaw)) -> goto accept_all
    :: (1) -> goto T0_init
  fi;
accept_all:
  skip
}