/**********************************************************************/
/***                                                                ***/
/***                     KEY AGREEMENT ALGORITHM                    ***/
/***                     SIMPLIFIED SECURE SPREAD                   ***/ 
/***                                                                ***/  
/***                                                                ***/ 
/***  Based on "Exploring Robustness in Group Key Agreement"        ***/
/***  by Amir, Kim, Nita-Rotaru, Schultz, Stanton, and Tsudik       ***/
/**********************************************************************/


/**********************************************************************/
/***    DATATYPES                                                   ***/   
/***                                                                ***/ 
/**********************************************************************/

TYPESPEC MSGTYPES;
TYPES MsgType: Field;       
CONSTANTS 
  Membership: MsgType;
  PartialToken: MsgType;
  FinalToken: MsgType;
  KeyList: MsgType;
  FactorOut: MsgType;
  Trans_Signal_Msg: MsgType;
END;

TYPESPEC PRINCIPALARRAY;
TYPES SParray[ ]: Principal;
END;

TYPESPEC SpreadARRAY;
FUNCTIONS
  minus(SParray,SParray): SParray;
  next(Principal,SParray): Principal; 
  alone(Principal,SParray): Boolean;
  isin(Principal,SParray): Boolean;
  pos(Principal,SParray): Nat;
  add(Principal,SParray): SParray;
  setequal(SParray,SParray): Boolean;
CONSTANTS
  panull: SParray;
VARIABLES
  PA: SParray;
  P: Principal;
  I: Nat;
AXIOMS
  alone(P,<<P>>);
  IF isin(P,PA) THEN PA[pos(P,PA)] = P ENDIF;
  /* need more axioms here */
END;  

/**********************************************************************/
/*** CLIQUES datatypes                                              ***/ 
/***         GML: array of CLQ_GM entries. For each CLQ_GM, there   ***/ 
/***              are member_name, shared_key, and last_partial_key ***/  
/***              defined                                           ***/   
/**********************************************************************/

TYPESPEC CLQ_CTX;
TYPES CLQ_CTX: GroupMember,MUTEX;
CONSTANTS g: Skey;
ATTRIBUTES
  p: Nat;      /* position in group_members_list */
  Np: Skey;    /* Mi's session random number */
  Ks: Skey;    /* current group shared key */
  M: SParray;  /* member list */
  KL: Sarray;  /* key list */
  PT: Skey;    /* Partial token */
  FT: Skey;    /* Final token */
END;

TYPESPEC GKA_CTX;         
TYPES GKA_CTX: CLQ_CTX;  
ATTRIBUTES
  /* current membership information */
  mb_id: Nat; /* group view unique id */
/*  mb_set: SParray; this should be the same as M */
  vs_set: SParray;
  merge_set: SParray;
  leave_set: SParray;
  Me: Principal;  /* assume initialized to owner */
END;

TYPESPEC LastCTX;
TYPES LastCTX: GKA_CTX;
ATTRIBUTES
  FO: Sarray;
  FMlist: SParray;
  m: Principal;
END;

/**********************************************************************/ 
/***       MEMBERSHIP protocol                                      ***/  
/***       Roles: Alone, New, Chosen, Last, Other                   ***/  
/**********************************************************************/

PROTOCOL Membership;

ROLE Alone: GKA_CTX;

MESSAGES
  <- mb_id,M,vs_set,merge_set,leave_set;
  ?M = <<owner(Alone)>>;
  p=1;
  NEW Np;           
  Ks = g^Np;
END Alone;


ROLE New: GKA_CTX;

ASSUMPTIONS
  p=0;     
  Me = owner(New);    

MESSAGES
  <- mb_id,M,vs_set,merge_set,leave_set;
  isin(Me,merge_set)=true;
  not((Me = last(merge_set)))=true;
  <- PT;
  p=pos(Me,M);
  NEW Np;
  -> next(Me,merge_set): PT^Np;

  <- FT;  /* wait for final token message */
  -> last(merge_set): Me, FT^(1/Np);

  <- KL;  /* wait for key list */
  Ks = KL[p]^Np;
END New;


ROLE Last: LastCTX;

ASSUMPTIONS
  p=0;   
  Me = owner(Last);  
    
MESSAGES
  <- mb_id,M,vs_set,merge_set,leave_set;
  last(merge_set) = Me;
  (size(M)>1) = true;
  <- PT;   /* wait for partial token message */
  p=size(M);

  /* sending out the final token message */
  ->: PT;

  /* wait for factor out messages */
  FMlist = panull;
  DO
    <- m,FO[pos(m,M)];
    FMlist = add(m,FMlist);
  UNTIL setequal(add(Me,FMlist),M);
  NEW Np;
  Ks = PT^Np;
  KL = (FO^^Np);
  -> : KL;
END Last;


/* current group controller in installed view  */
ROLE Chosen: GKA_CTX;

ASSUMPTIONS
  Me = owner(Chosen);

MESSAGES
  <- mb_id,M,vs_set,merge_set,leave_set;
  last(vs_set) = Me;
  (size(merge_set)>0) = true;
  p = size(vs_set);
  NEW Np;
  -> merge_set[1]:  PT^Np; /* first new PT msg */
  
  <- FT;  /* wait for final token message */
  -> last(merge_set): Me, FT^(1/Np);

  <- KL;  /* wait for key list */
  Ks = KL[p]^Np;
END Chosen;


ROLE Other: GKA_CTX;

ASSUMPTIONS
  p>0; /* not a new member */
  Me = owner(Other);

MESSAGES
  <- mb_id,M,vs_set,merge_set,leave_set;
  isin(Me,vs_set)=true;
  not((Me = last(vs_set)))=true; 
  <- FT;  /* wait for final token message */
  -> last(merge_set): Me, FT^(1/Np);
  <- KL;  /* wait for key list */
  Ks = KL[p]^Np;
END Other;

ROLE Flush: GKA_CTX;

CONSTANTS flush: Atom;

MESSAGES
  <- flush;
  ABORT;
END Flush;


END Membership;

ENVIRONMENT e1;

CONSTANTS
  Alice,Bob: Principal;
  gid: Nat;

MEMBER MAlice(Alice,gid): LastCTX; 
  Me = Alice;
  p = 1;
  M = <<MAlice>>;

MEMBER MBob(Bob,gid): LastCTX;
  Me = Bob;
  p = 0;

STATE MemberShipAlone(MAlice);

STATE MemberShipNew(MBob);

END e1;