# GSFedSec: Group Signature-Based Secure Aggregation for Privacy Preservation in Federated Learning
## Appendix B Simulation Code of the Security Proof  
This appendix gives the simulation code of the various roles in our algorithm. This is carried out using HLPSL language, and execution is carried out in the AVISPA tool. Details of the coding-related information can be found in Section 4. ```
roleanalyst(A,S,C1,C2,C3,C4:agent, Snd,Rcv:channel(dy)) played_byA def= localState:nat, SecA,SecS:symmetric_key, PubC,PubS:public_key, LatestModel,Data:text initState:=0 transition 1.State=0/Rcv(start)=|> State':=1/L Latest_Model:=new() /PubC:=new() /Snd(LatestModel')
2.State=1/Rcv(Data')_PubS=1> State':=2/Snd(LatestModel) endrole ListingA2. Role Server. roleserver(S,A,C1,C2,C3,C4:agent, Snd,Rcv:channel(dy)) played_byS def= localState:nat, PubS,PubC:public_key, Req1,Req2,Req3,Req4, Cdata1,Cdata2,Cdata4,Data, Acc1,Acc2,Acc4:text, SecA,SecS,RAND1,RAND2,RAND3, RANDM,Gsign:symmetric_key constsec_S_C1,sec_S_C2, sec_S_C4:protocol_id initState:=1 transition
```1. State = 1 / \(\cdot\) Rev(Req1_Gsign_RAND1_Puh8) / \(\cdot\) Rev(Req2_Gsign_RAND2_Puh8) / \(\cdot\) Rev(Req3_Gsign_RAND3_Puh8) / \(\cdot\) Rev(Req4_Gsign_RAND4_Puh8)=1> State ':= 2 /\(\cdot\) Snd(Acc1_RAND1) / \(\cdot\) Snd(Acc2_RAND2) / \(\cdot\) Snd(Acc2_RAND4)
2. State = 2 /\(\cdot\) Rev(Catal_Gsign) / \(\cdot\) Rev(Cdata2_Gsign) / \(\cdot\) Rev(Cdata4_Gsign) =1> State ':= 3 /\(\cdot\) Data:= new() /\(\cdot\) Snd(Data)_Puh8 / secret(Cdata1,sec_S_C1,{S,C1}) /\(\cdot\) secret(Cdata2,sec_S_C2,{S,C2}) /\(\cdot\) secret(Cdata4,sec_S_C4,{S,C4}) /\(\cdot\) witness(D1,S,rand1_auth,RAND1) /\(\cdot\) witness(D2,S,rand2_auth,RAND2) /\(\cdot\) witness(D3,S,rand3_auth,RAND4) /\(\cdot\) witness(D4,S,rand4_auth,RAND4) end role Listing A3. Role Client1. role client1 (A,S,C1: agent,  Snd,Recv: channel(dy)) played_by C1  def= localState: nat,  Cdata1,Acc1,LatestModel: text,  RANDI,Gsign: symmetric_key,  PubC1: public_key const sec_S_C1 : protocol_id init State := 0 transition 1. State = 0 /\(\cdot\) Rev(Gsign.PubC1) /\(\cdot\)Rev(LatestModel) =1> State ':= 1 /\(\cdot\) Req1':= new() /\(\cdot\) RANDI':= new() /\(\cdot\) Snd([Req1']_Gsign_RAND1_Puh8)
2. State = 1 /\(\cdot\) Rev(Acc1_RAND1)=1> State ':= 2 /\(\cdot\) Cdata1 := new() /\(\cdot\)Snd(Cdata1'_Puh8) /\(\cdot\) secret(Cdata1,sec_S_C1,{S,C1}) /\(\cdot\) wrequest(DI,S,rand1_auth,RAND1) end role Listing A4. Role Client2. role client2 (A,S,C2: agent,  Snd,Recv: channel(dy)) played_by C2 def= localState: nat,  Cdata2,Acc2,LatestModel: text,  RAND2,Gsign: symmetric_key,  PubC2: public_key const sec_S_C2: protocol_id init State := 0 transition 1. State = 0 /\(\cdot\) Rev(Gsign.PubC2) /\(\cdot\)Rev(LatestModel) =1>State':=1/Req2':=new()  /RAND2':=new()  /Snd(|Req2'|_Csign.RAND2_Pub5)
2. State=1/Rev(Acc2_RAND2)=1>  State':=2/Cdata2:=new()  /Snd(Cdata2'_Pub5)  /secret(Cdata2,sec_S_C2,{S,C2})  /\wrequest(D2,S,rand_2_auth,RAND2) endrole  
**Listing A5**. Role Client3. roleclient3(A,S,C3:agent,  Snd,Rcv:channel(dy)) played_byC3 def=  localState:nat,  Cdata3,Acc3,LatestModel:text,  RANDB,Gsign:symmetric_key,  PubC3:public_key  
constsec_S_c3:protocol_id  
initState:=0 transition  1.State=0/Rcv(Csign.PubC3)  /Rcv(LatestModel)=1>  State':=1/Req3':=new()  /RAND3':=new()  /Snd(|Req3'|_Csign.RAND3_Pub5)  /\wrequest(D3,S,rand3_auth,RAND3) endrole  
**Listing A6**. Role Client4. roleclient4(A,S,C4:agent,  
Snd,Rcv:channel(dy))  
played_byC4 def=  localState:nat,  Cdata4,Acc4,LatestModel:text,  RANDB,Gsign:symmetric_key,  PubC4:public_key  
constsec_S_C4:protocol_id  
initState:=0 transition  1.State=0/Rcv(Csign.PubC4)  /\Rcv(LatestModel)=1>  State':=1/Req4':=new()  /RAND4':=new()  /\Snd(|Req4'|_Csign.RAND1_Pub5)  
2.State=1/Rcv(Acc4_RAND4)=1>  State':=2/Cdata4:=new()  /Snd(Cdata4'_Pub5)  /\screct(Cdata4,sec_S_C4,{S,C4})  /\wrequest(D4,S,rand_auth,RAND4) endrole```
Listing A7: Role Admin. role admin (A2,C1,C2,C3,C4: agent, Snd,Rev: channel(dy))
``` played_byA2 def= localState:nat, Gsign:public_key constsec_A2_C4,sec_A2_C2, sec_A2_C3,sec_A2_C1:protocol_id initState:=0 transition
1.