pred att/2. pred mess/3. fun aenc/3. fun bt/1. fun h/2. fun md5/1. fun pk/1. fun senc/2. fun tuple2/2. fun tuple3/3. param simplifyDerivation = true. param redundantHypElim = true. param redundancyElim = best. param selFun = Term. query att:u,pwd'4[]. query att:u,allow_login[]. (* Sanity check *) nounif att:*u,x. nounif mess:*u,*vc,vm. reduc (* Clauses corresponding to mutability of cells *) (* Clauses corresponding to the attacker's ability to apply constructors *) att:tuple3(xBoot,u0[],xFlag),x_1 & att:tuple3(xBoot,u0[],xFlag),x_2 & att:tuple3(xBoot,u0[],xFlag),x_3 -> att:tuple3(xBoot,u0[],xFlag),aenc(x_1,x_2,x_3); (* applying aenc *) att:tuple3(xBoot,h(u0[],v1),xFlag),x_1 & att:tuple3(xBoot,h(u0[],v1),xFlag),x_2 & att:tuple3(xBoot,h(u0[],v1),xFlag),x_3 -> att:tuple3(xBoot,h(u0[],v1),xFlag),aenc(x_1,x_2,x_3); (* applying aenc *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_1 & att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_2 & att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_3 -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),aenc(x_1,x_2,x_3); (* applying aenc *) att:tuple3(xBoot,u1[],xFlag),x_1 & att:tuple3(xBoot,u1[],xFlag),x_2 & att:tuple3(xBoot,u1[],xFlag),x_3 -> att:tuple3(xBoot,u1[],xFlag),aenc(x_1,x_2,x_3); (* applying aenc *) att:tuple3(xBoot,h(u1[],v3),xFlag),x_1 & att:tuple3(xBoot,h(u1[],v3),xFlag),x_2 & att:tuple3(xBoot,h(u1[],v3),xFlag),x_3 -> att:tuple3(xBoot,h(u1[],v3),xFlag),aenc(x_1,x_2,x_3); (* applying aenc *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_1 & att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_2 & att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_3 -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),aenc(x_1,x_2,x_3); (* applying aenc *) att:tuple3(xBoot,u0[],xFlag),x_1 & att:tuple3(xBoot,u0[],xFlag),x_2 -> att:tuple3(xBoot,u0[],xFlag),h(x_1,x_2); (* applying h *) att:tuple3(xBoot,h(u0[],v1),xFlag),x_1 & att:tuple3(xBoot,h(u0[],v1),xFlag),x_2 -> att:tuple3(xBoot,h(u0[],v1),xFlag),h(x_1,x_2); (* applying h *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_1 & att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_2 -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),h(x_1,x_2); (* applying h *) att:tuple3(xBoot,u1[],xFlag),x_1 & att:tuple3(xBoot,u1[],xFlag),x_2 -> att:tuple3(xBoot,u1[],xFlag),h(x_1,x_2); (* applying h *) att:tuple3(xBoot,h(u1[],v3),xFlag),x_1 & att:tuple3(xBoot,h(u1[],v3),xFlag),x_2 -> att:tuple3(xBoot,h(u1[],v3),xFlag),h(x_1,x_2); (* applying h *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_1 & att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_2 -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),h(x_1,x_2); (* applying h *) att:tuple3(xBoot,u0[],xFlag),x_1 -> att:tuple3(xBoot,u0[],xFlag),md5(x_1); (* applying md5 *) att:tuple3(xBoot,h(u0[],v1),xFlag),x_1 -> att:tuple3(xBoot,h(u0[],v1),xFlag),md5(x_1); (* applying md5 *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_1 -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),md5(x_1); (* applying md5 *) att:tuple3(xBoot,u1[],xFlag),x_1 -> att:tuple3(xBoot,u1[],xFlag),md5(x_1); (* applying md5 *) att:tuple3(xBoot,h(u1[],v3),xFlag),x_1 -> att:tuple3(xBoot,h(u1[],v3),xFlag),md5(x_1); (* applying md5 *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_1 -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),md5(x_1); (* applying md5 *) att:tuple3(xBoot,u0[],xFlag),x_1 -> att:tuple3(xBoot,u0[],xFlag),pk(x_1); (* applying pk *) att:tuple3(xBoot,h(u0[],v1),xFlag),x_1 -> att:tuple3(xBoot,h(u0[],v1),xFlag),pk(x_1); (* applying pk *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_1 -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),pk(x_1); (* applying pk *) att:tuple3(xBoot,u1[],xFlag),x_1 -> att:tuple3(xBoot,u1[],xFlag),pk(x_1); (* applying pk *) att:tuple3(xBoot,h(u1[],v3),xFlag),x_1 -> att:tuple3(xBoot,h(u1[],v3),xFlag),pk(x_1); (* applying pk *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_1 -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),pk(x_1); (* applying pk *) att:tuple3(xBoot,u0[],xFlag),x_1 & att:tuple3(xBoot,u0[],xFlag),x_2 -> att:tuple3(xBoot,u0[],xFlag),senc(x_1,x_2); (* applying senc *) att:tuple3(xBoot,h(u0[],v1),xFlag),x_1 & att:tuple3(xBoot,h(u0[],v1),xFlag),x_2 -> att:tuple3(xBoot,h(u0[],v1),xFlag),senc(x_1,x_2); (* applying senc *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_1 & att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_2 -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),senc(x_1,x_2); (* applying senc *) att:tuple3(xBoot,u1[],xFlag),x_1 & att:tuple3(xBoot,u1[],xFlag),x_2 -> att:tuple3(xBoot,u1[],xFlag),senc(x_1,x_2); (* applying senc *) att:tuple3(xBoot,h(u1[],v3),xFlag),x_1 & att:tuple3(xBoot,h(u1[],v3),xFlag),x_2 -> att:tuple3(xBoot,h(u1[],v3),xFlag),senc(x_1,x_2); (* applying senc *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_1 & att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_2 -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),senc(x_1,x_2); (* applying senc *) att:tuple3(xBoot,u0[],xFlag),x_1 & att:tuple3(xBoot,u0[],xFlag),x_2 -> att:tuple3(xBoot,u0[],xFlag),tuple2(x_1,x_2); (* applying tuple2 *) att:tuple3(xBoot,h(u0[],v1),xFlag),x_1 & att:tuple3(xBoot,h(u0[],v1),xFlag),x_2 -> att:tuple3(xBoot,h(u0[],v1),xFlag),tuple2(x_1,x_2); (* applying tuple2 *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_1 & att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_2 -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),tuple2(x_1,x_2); (* applying tuple2 *) att:tuple3(xBoot,u1[],xFlag),x_1 & att:tuple3(xBoot,u1[],xFlag),x_2 -> att:tuple3(xBoot,u1[],xFlag),tuple2(x_1,x_2); (* applying tuple2 *) att:tuple3(xBoot,h(u1[],v3),xFlag),x_1 & att:tuple3(xBoot,h(u1[],v3),xFlag),x_2 -> att:tuple3(xBoot,h(u1[],v3),xFlag),tuple2(x_1,x_2); (* applying tuple2 *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_1 & att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_2 -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),tuple2(x_1,x_2); (* applying tuple2 *) att:tuple3(xBoot,u0[],xFlag),x_1 & att:tuple3(xBoot,u0[],xFlag),x_2 & att:tuple3(xBoot,u0[],xFlag),x_3 -> att:tuple3(xBoot,u0[],xFlag),tuple3(x_1,x_2,x_3); (* applying tuple3 *) att:tuple3(xBoot,h(u0[],v1),xFlag),x_1 & att:tuple3(xBoot,h(u0[],v1),xFlag),x_2 & att:tuple3(xBoot,h(u0[],v1),xFlag),x_3 -> att:tuple3(xBoot,h(u0[],v1),xFlag),tuple3(x_1,x_2,x_3); (* applying tuple3 *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_1 & att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_2 & att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x_3 -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),tuple3(x_1,x_2,x_3); (* applying tuple3 *) att:tuple3(xBoot,u1[],xFlag),x_1 & att:tuple3(xBoot,u1[],xFlag),x_2 & att:tuple3(xBoot,u1[],xFlag),x_3 -> att:tuple3(xBoot,u1[],xFlag),tuple3(x_1,x_2,x_3); (* applying tuple3 *) att:tuple3(xBoot,h(u1[],v3),xFlag),x_1 & att:tuple3(xBoot,h(u1[],v3),xFlag),x_2 & att:tuple3(xBoot,h(u1[],v3),xFlag),x_3 -> att:tuple3(xBoot,h(u1[],v3),xFlag),tuple3(x_1,x_2,x_3); (* applying tuple3 *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_1 & att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_2 & att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x_3 -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),tuple3(x_1,x_2,x_3); (* applying tuple3 *) (* Clauses corresponding to the attacker's ability to apply reductions *) att:tuple3(xBoot,u0[],xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,u0[],xFlag),z; (* applying trd3 *) att:tuple3(xBoot,h(u0[],v1),xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,h(u0[],v1),xFlag),z; (* applying trd3 *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),z; (* applying trd3 *) att:tuple3(xBoot,u1[],xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,u1[],xFlag),z; (* applying trd3 *) att:tuple3(xBoot,h(u1[],v3),xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,h(u1[],v3),xFlag),z; (* applying trd3 *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),z; (* applying trd3 *) att:tuple3(xBoot,u0[],xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,u0[],xFlag),y; (* applying snd3 *) att:tuple3(xBoot,h(u0[],v1),xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,h(u0[],v1),xFlag),y; (* applying snd3 *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),y; (* applying snd3 *) att:tuple3(xBoot,u1[],xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,u1[],xFlag),y; (* applying snd3 *) att:tuple3(xBoot,h(u1[],v3),xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,h(u1[],v3),xFlag),y; (* applying snd3 *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),y; (* applying snd3 *) att:tuple3(xBoot,u0[],xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,u0[],xFlag),x; (* applying fst3 *) att:tuple3(xBoot,h(u0[],v1),xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,h(u0[],v1),xFlag),x; (* applying fst3 *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x; (* applying fst3 *) att:tuple3(xBoot,u1[],xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,u1[],xFlag),x; (* applying fst3 *) att:tuple3(xBoot,h(u1[],v3),xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,h(u1[],v3),xFlag),x; (* applying fst3 *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),tuple3(x,y,z) -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x; (* applying fst3 *) att:tuple3(xBoot,u0[],xFlag),tuple2(x,y) -> att:tuple3(xBoot,u0[],xFlag),y; (* applying snd2 *) att:tuple3(xBoot,h(u0[],v1),xFlag),tuple2(x,y) -> att:tuple3(xBoot,h(u0[],v1),xFlag),y; (* applying snd2 *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),tuple2(x,y) -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),y; (* applying snd2 *) att:tuple3(xBoot,u1[],xFlag),tuple2(x,y) -> att:tuple3(xBoot,u1[],xFlag),y; (* applying snd2 *) att:tuple3(xBoot,h(u1[],v3),xFlag),tuple2(x,y) -> att:tuple3(xBoot,h(u1[],v3),xFlag),y; (* applying snd2 *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),tuple2(x,y) -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),y; (* applying snd2 *) att:tuple3(xBoot,u0[],xFlag),tuple2(x,y) -> att:tuple3(xBoot,u0[],xFlag),x; (* applying fst2 *) att:tuple3(xBoot,h(u0[],v1),xFlag),tuple2(x,y) -> att:tuple3(xBoot,h(u0[],v1),xFlag),x; (* applying fst2 *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),tuple2(x,y) -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x; (* applying fst2 *) att:tuple3(xBoot,u1[],xFlag),tuple2(x,y) -> att:tuple3(xBoot,u1[],xFlag),x; (* applying fst2 *) att:tuple3(xBoot,h(u1[],v3),xFlag),tuple2(x,y) -> att:tuple3(xBoot,h(u1[],v3),xFlag),x; (* applying fst2 *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),tuple2(x,y) -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x; (* applying fst2 *) att:tuple3(xBoot,u0[],xFlag),x & att:tuple3(xBoot,u0[],xFlag),aenc(pk(x),y,z) -> att:tuple3(xBoot,u0[],xFlag),z; (* applying adec *) att:tuple3(xBoot,h(u0[],v1),xFlag),x & att:tuple3(xBoot,h(u0[],v1),xFlag),aenc(pk(x),y,z) -> att:tuple3(xBoot,h(u0[],v1),xFlag),z; (* applying adec *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x & att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),aenc(pk(x),y,z) -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),z; (* applying adec *) att:tuple3(xBoot,u1[],xFlag),x & att:tuple3(xBoot,u1[],xFlag),aenc(pk(x),y,z) -> att:tuple3(xBoot,u1[],xFlag),z; (* applying adec *) att:tuple3(xBoot,h(u1[],v3),xFlag),x & att:tuple3(xBoot,h(u1[],v3),xFlag),aenc(pk(x),y,z) -> att:tuple3(xBoot,h(u1[],v3),xFlag),z; (* applying adec *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x & att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),aenc(pk(x),y,z) -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),z; (* applying adec *) att:tuple3(xBoot,u0[],xFlag),x & att:tuple3(xBoot,u0[],xFlag),senc(x,y) -> att:tuple3(xBoot,u0[],xFlag),y; (* applying sdec *) att:tuple3(xBoot,h(u0[],v1),xFlag),x & att:tuple3(xBoot,h(u0[],v1),xFlag),senc(x,y) -> att:tuple3(xBoot,h(u0[],v1),xFlag),y; (* applying sdec *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),x & att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),senc(x,y) -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),y; (* applying sdec *) att:tuple3(xBoot,u1[],xFlag),x & att:tuple3(xBoot,u1[],xFlag),senc(x,y) -> att:tuple3(xBoot,u1[],xFlag),y; (* applying sdec *) att:tuple3(xBoot,h(u1[],v3),xFlag),x & att:tuple3(xBoot,h(u1[],v3),xFlag),senc(x,y) -> att:tuple3(xBoot,h(u1[],v3),xFlag),y; (* applying sdec *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),x & att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),senc(x,y) -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),y; (* applying sdec *) (* Clauses corresponding to the attacker's ability to use channels it knows *) mess:tuple3(xBoot,u0[],xFlag),vc,vm & att:tuple3(xBoot,u0[],xFlag),vc -> att:tuple3(xBoot,u0[],xFlag),vm; (* receiving *) mess:tuple3(xBoot,h(u0[],v1),xFlag),vc,vm & att:tuple3(xBoot,h(u0[],v1),xFlag),vc -> att:tuple3(xBoot,h(u0[],v1),xFlag),vm; (* receiving *) mess:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),vc,vm & att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),vc -> att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),vm; (* receiving *) mess:tuple3(xBoot,u1[],xFlag),vc,vm & att:tuple3(xBoot,u1[],xFlag),vc -> att:tuple3(xBoot,u1[],xFlag),vm; (* receiving *) mess:tuple3(xBoot,h(u1[],v3),xFlag),vc,vm & att:tuple3(xBoot,h(u1[],v3),xFlag),vc -> att:tuple3(xBoot,h(u1[],v3),xFlag),vm; (* receiving *) mess:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),vc,vm & att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),vc -> att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),vm; (* receiving *) att:tuple3(xBoot,u0[],xFlag),vc & att:tuple3(xBoot,u0[],xFlag),vm -> mess:tuple3(xBoot,u0[],xFlag),vc,vm; (* sending *) att:tuple3(xBoot,h(u0[],v1),xFlag),vc & att:tuple3(xBoot,h(u0[],v1),xFlag),vm -> mess:tuple3(xBoot,h(u0[],v1),xFlag),vc,vm; (* sending *) att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),vc & att:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),vm -> mess:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),vc,vm; (* sending *) att:tuple3(xBoot,u1[],xFlag),vc & att:tuple3(xBoot,u1[],xFlag),vm -> mess:tuple3(xBoot,u1[],xFlag),vc,vm; (* sending *) att:tuple3(xBoot,h(u1[],v3),xFlag),vc & att:tuple3(xBoot,h(u1[],v3),xFlag),vm -> mess:tuple3(xBoot,h(u1[],v3),xFlag),vc,vm; (* sending *) att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),vc & att:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),vm -> mess:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),vc,vm; (* sending *) (* Knowledge of free names *) att:tuple3(b0[],u1[],false[]),attch[]; (* attacker's own channel *) att:tuple3(b0[],u1[],false[]),attn[]; (* attacker's own nonce *) att:tuple3(b0[],u1[],false[]),unseal[]; att:tuple3(b0[],u1[],false[]),seal[]; att:tuple3(b0[],u1[],false[]),extend[]; att:tuple3(b0[],u1[],false[]),slbA[]; att:tuple3(b0[],u1[],false[]),fpc[]; att:tuple3(b0[],u1[],false[]),u1[]; att:tuple3(b0[],u1[],false[]),u0[]; att:tuple3(b0[],u1[],false[]),loc2pub[]; att:tuple3(b0[],u1[],false[]),c[]; (* Clauses from the process *) mess:tuple3(b0[],u1[],false[]),c[],pk(skSrk'2[]); (* output on l.181 *) mess:tuple3(b0[],u1[],false[]),c[],pk(skSlb'3[]); (* output on l.184 *) mess:tuple3(b0[],u1[],false[]),c[],salt'5[]; (* output on l.188 *) mess:tuple3(b0[],u1[],false[]),c[],aenc(pk(skSrk'2[]),r'6[],tuple3(tpmPf[],h(u0[],slbA[]),skSlb'3[])); (* output on l.191 *) mess:tuple3(xBoot,u0[],xFlag),loc2priv[],tuple2(unseal[],aenc(pk(skSrk'2[]),y_14,tuple3(tpmPf[],u0[],z_16))) -> mess:tuple3(xBoot,u0[],xFlag),loc2priv[],z_16; (* output on l.118 *) mess:tuple3(xBoot,h(u0[],v1),xFlag),loc2priv[],tuple2(unseal[],aenc(pk(skSrk'2[]),y_14,tuple3(tpmPf[],h(u0[],v1),z_16))) -> mess:tuple3(xBoot,h(u0[],v1),xFlag),loc2priv[],z_16; (* output on l.118 *) mess:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),loc2priv[],tuple2(unseal[],aenc(pk(skSrk'2[]),y_14,tuple3(tpmPf[],h(h(u0[],v1),v2),z_16))) -> mess:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),loc2priv[],z_16; (* output on l.118 *) mess:tuple3(xBoot,u1[],xFlag),loc2priv[],tuple2(unseal[],aenc(pk(skSrk'2[]),y_14,tuple3(tpmPf[],u1[],z_16))) -> mess:tuple3(xBoot,u1[],xFlag),loc2priv[],z_16; (* output on l.118 *) mess:tuple3(xBoot,h(u1[],v3),xFlag),loc2priv[],tuple2(unseal[],aenc(pk(skSrk'2[]),y_14,tuple3(tpmPf[],h(u1[],v3),z_16))) -> mess:tuple3(xBoot,h(u1[],v3),xFlag),loc2priv[],z_16; (* output on l.118 *) mess:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),loc2priv[],tuple2(unseal[],aenc(pk(skSrk'2[]),y_14,tuple3(tpmPf[],h(h(u1[],v3),v4),z_16))) -> mess:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),loc2priv[],z_16; (* output on l.118 *) mess:tuple3(xBoot,u0[],false[]),loc2pub[],tuple2(extend[],y_20) & mess:tuple3(xBoot,u0[],false[]),vc22,vm22 -> mess:tuple3(xBoot,h(u0[],y_20),false[]),vc22,vm22; (* assignment on l.140 *) mess:tuple3(xBoot,h(u0[],v1),false[]),loc2pub[],tuple2(extend[],y_20) & mess:tuple3(xBoot,h(u0[],v1),false[]),vc22,vm22 -> mess:tuple3(xBoot,h(h(u0[],v1),y_20),false[]),vc22,vm22; (* assignment on l.140 *) mess:tuple3(xBoot,h(h(u0[],v1),v2),false[]),loc2pub[],tuple2(extend[],y_20) & mess:tuple3(xBoot,h(h(u0[],v1),v2),false[]),vc22,vm22 -> mess:tuple3(xBoot,h(h(h(u0[],v1),v2),y_20),false[]),vc22,vm22; (* assignment on l.140 *) mess:tuple3(xBoot,u1[],false[]),loc2pub[],tuple2(extend[],y_20) & mess:tuple3(xBoot,u1[],false[]),vc22,vm22 -> mess:tuple3(xBoot,h(u1[],y_20),false[]),vc22,vm22; (* assignment on l.140 *) mess:tuple3(xBoot,h(u1[],v3),false[]),loc2pub[],tuple2(extend[],y_20) & mess:tuple3(xBoot,h(u1[],v3),false[]),vc22,vm22 -> mess:tuple3(xBoot,h(h(u1[],v3),y_20),false[]),vc22,vm22; (* assignment on l.140 *) mess:tuple3(xBoot,h(h(u1[],v3),v4),false[]),loc2pub[],tuple2(extend[],y_20) & mess:tuple3(xBoot,h(h(u1[],v3),v4),false[]),vc22,vm22 -> mess:tuple3(xBoot,h(h(h(u1[],v3),v4),y_20),false[]),vc22,vm22; (* assignment on l.140 *) mess:tuple3(xBoot,u0[],false[]),loc2pub[],tuple2(extend[],y_20) & att:tuple3(xBoot,u0[],false[]),vm22 -> att:tuple3(xBoot,h(u0[],y_20),false[]),vm22; (* assignment on l.140 *) mess:tuple3(xBoot,h(u0[],v1),false[]),loc2pub[],tuple2(extend[],y_20) & att:tuple3(xBoot,h(u0[],v1),false[]),vm22 -> att:tuple3(xBoot,h(h(u0[],v1),y_20),false[]),vm22; (* assignment on l.140 *) mess:tuple3(xBoot,h(h(u0[],v1),v2),false[]),loc2pub[],tuple2(extend[],y_20) & att:tuple3(xBoot,h(h(u0[],v1),v2),false[]),vm22 -> att:tuple3(xBoot,h(h(h(u0[],v1),v2),y_20),false[]),vm22; (* assignment on l.140 *) mess:tuple3(xBoot,u1[],false[]),loc2pub[],tuple2(extend[],y_20) & att:tuple3(xBoot,u1[],false[]),vm22 -> att:tuple3(xBoot,h(u1[],y_20),false[]),vm22; (* assignment on l.140 *) mess:tuple3(xBoot,h(u1[],v3),false[]),loc2pub[],tuple2(extend[],y_20) & att:tuple3(xBoot,h(u1[],v3),false[]),vm22 -> att:tuple3(xBoot,h(h(u1[],v3),y_20),false[]),vm22; (* assignment on l.140 *) mess:tuple3(xBoot,h(h(u1[],v3),v4),false[]),loc2pub[],tuple2(extend[],y_20) & att:tuple3(xBoot,h(h(u1[],v3),v4),false[]),vm22 -> att:tuple3(xBoot,h(h(h(u1[],v3),v4),y_20),false[]),vm22; (* assignment on l.140 *) mess:tuple3(xBoot,u0[],false[]),loc2pub[],tuple2(unseal[],aenc(pk(skSrk'2[]),y_23,tuple3(tpmPf[],u0[],z_25))) -> mess:tuple3(xBoot,u0[],false[]),loc2pub[],z_25; (* output on l.154 *) mess:tuple3(xBoot,h(u0[],v1),false[]),loc2pub[],tuple2(unseal[],aenc(pk(skSrk'2[]),y_23,tuple3(tpmPf[],h(u0[],v1),z_25))) -> mess:tuple3(xBoot,h(u0[],v1),false[]),loc2pub[],z_25; (* output on l.154 *) mess:tuple3(xBoot,h(h(u0[],v1),v2),false[]),loc2pub[],tuple2(unseal[],aenc(pk(skSrk'2[]),y_23,tuple3(tpmPf[],h(h(u0[],v1),v2),z_25))) -> mess:tuple3(xBoot,h(h(u0[],v1),v2),false[]),loc2pub[],z_25; (* output on l.154 *) mess:tuple3(xBoot,u1[],false[]),loc2pub[],tuple2(unseal[],aenc(pk(skSrk'2[]),y_23,tuple3(tpmPf[],u1[],z_25))) -> mess:tuple3(xBoot,u1[],false[]),loc2pub[],z_25; (* output on l.154 *) mess:tuple3(xBoot,h(u1[],v3),false[]),loc2pub[],tuple2(unseal[],aenc(pk(skSrk'2[]),y_23,tuple3(tpmPf[],h(u1[],v3),z_25))) -> mess:tuple3(xBoot,h(u1[],v3),false[]),loc2pub[],z_25; (* output on l.154 *) mess:tuple3(xBoot,h(h(u1[],v3),v4),false[]),loc2pub[],tuple2(unseal[],aenc(pk(skSrk'2[]),y_23,tuple3(tpmPf[],h(h(u1[],v3),v4),z_25))) -> mess:tuple3(xBoot,h(h(u1[],v3),v4),false[]),loc2pub[],z_25; (* output on l.154 *) mess:tuple3(xBoot,u0[],false[]),loc2pub[],tuple3(seal[],y_18,z_19) -> mess:tuple3(xBoot,u0[],false[]),loc2pub[],aenc(pk(skSrk'2[]),r'7[],tuple3(tpmPf[],y_18,z_19)); (* output on l.165 *) mess:tuple3(xBoot,h(u0[],v1),false[]),loc2pub[],tuple3(seal[],y_18,z_19) -> mess:tuple3(xBoot,h(u0[],v1),false[]),loc2pub[],aenc(pk(skSrk'2[]),r'7[],tuple3(tpmPf[],y_18,z_19)); (* output on l.165 *) mess:tuple3(xBoot,h(h(u0[],v1),v2),false[]),loc2pub[],tuple3(seal[],y_18,z_19) -> mess:tuple3(xBoot,h(h(u0[],v1),v2),false[]),loc2pub[],aenc(pk(skSrk'2[]),r'7[],tuple3(tpmPf[],y_18,z_19)); (* output on l.165 *) mess:tuple3(xBoot,u1[],false[]),loc2pub[],tuple3(seal[],y_18,z_19) -> mess:tuple3(xBoot,u1[],false[]),loc2pub[],aenc(pk(skSrk'2[]),r'7[],tuple3(tpmPf[],y_18,z_19)); (* output on l.165 *) mess:tuple3(xBoot,h(u1[],v3),false[]),loc2pub[],tuple3(seal[],y_18,z_19) -> mess:tuple3(xBoot,h(u1[],v3),false[]),loc2pub[],aenc(pk(skSrk'2[]),r'7[],tuple3(tpmPf[],y_18,z_19)); (* output on l.165 *) mess:tuple3(xBoot,h(h(u1[],v3),v4),false[]),loc2pub[],tuple3(seal[],y_18,z_19) -> mess:tuple3(xBoot,h(h(u1[],v3),v4),false[]),loc2pub[],aenc(pk(skSrk'2[]),r'7[],tuple3(tpmPf[],y_18,z_19)); (* output on l.165 *) mess:tuple3(b0[],u0[],false[]),vc17,vm17 -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vc17,vm17; (* assignment on l.64 *) mess:tuple3(b0[],h(u0[],v1),false[]),vc17,vm17 -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vc17,vm17; (* assignment on l.64 *) mess:tuple3(b0[],h(h(u0[],v1),v2),false[]),vc17,vm17 -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vc17,vm17; (* assignment on l.64 *) mess:tuple3(b0[],u1[],false[]),vc17,vm17 -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vc17,vm17; (* assignment on l.64 *) mess:tuple3(b0[],h(u1[],v3),false[]),vc17,vm17 -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vc17,vm17; (* assignment on l.64 *) mess:tuple3(b0[],h(h(u1[],v3),v4),false[]),vc17,vm17 -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vc17,vm17; (* assignment on l.64 *) att:tuple3(b0[],u0[],false[]),vm17 -> att:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vm17; (* assignment on l.64 *) att:tuple3(b0[],h(u0[],v1),false[]),vm17 -> att:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vm17; (* assignment on l.64 *) att:tuple3(b0[],h(h(u0[],v1),v2),false[]),vm17 -> att:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vm17; (* assignment on l.64 *) att:tuple3(b0[],u1[],false[]),vm17 -> att:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vm17; (* assignment on l.64 *) att:tuple3(b0[],h(u1[],v3),false[]),vm17 -> att:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vm17; (* assignment on l.64 *) att:tuple3(b0[],h(h(u1[],v3),v4),false[]),vm17 -> att:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vm17; (* assignment on l.64 *) mess:tuple3(b0[],u0[],false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xCipher & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xNonce -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],tuple2(unseal[],xSdata); (* output on l.71 *) mess:tuple3(b0[],h(u0[],v1),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xCipher & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xNonce -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],tuple2(unseal[],xSdata); (* output on l.71 *) mess:tuple3(b0[],h(h(u0[],v1),v2),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xCipher & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xNonce -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],tuple2(unseal[],xSdata); (* output on l.71 *) mess:tuple3(b0[],u1[],false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xCipher & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xNonce -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],tuple2(unseal[],xSdata); (* output on l.71 *) mess:tuple3(b0[],h(u1[],v3),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xCipher & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xNonce -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],tuple2(unseal[],xSdata); (* output on l.71 *) mess:tuple3(b0[],h(h(u1[],v3),v4),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xCipher & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xNonce -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],tuple2(unseal[],xSdata); (* output on l.71 *) mess:tuple3(b0[],u0[],false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],md5(tuple2(xSalt,xPwd)); (* output on l.78 *) mess:tuple3(b0[],h(u0[],v1),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],md5(tuple2(xSalt,xPwd)); (* output on l.78 *) mess:tuple3(b0[],h(h(u0[],v1),v2),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],md5(tuple2(xSalt,xPwd)); (* output on l.78 *) mess:tuple3(b0[],u1[],false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],md5(tuple2(xSalt,xPwd)); (* output on l.78 *) mess:tuple3(b0[],h(u1[],v3),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],md5(tuple2(xSalt,xPwd)); (* output on l.78 *) mess:tuple3(b0[],h(h(u1[],v3),v4),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb -> mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],md5(tuple2(xSalt,xPwd)); (* output on l.78 *) mess:tuple3(b0[],u0[],false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vc32,vm32 -> mess:tuple3(bt(b0[]),h(h(u0[],slbA[]),fpc[]),false[]),vc32,vm32; (* assignment on l.84 *) mess:tuple3(b0[],h(u0[],v1),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vc32,vm32 -> mess:tuple3(bt(b0[]),h(h(u0[],slbA[]),fpc[]),false[]),vc32,vm32; (* assignment on l.84 *) mess:tuple3(b0[],h(h(u0[],v1),v2),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vc32,vm32 -> mess:tuple3(bt(b0[]),h(h(u0[],slbA[]),fpc[]),false[]),vc32,vm32; (* assignment on l.84 *) mess:tuple3(b0[],u1[],false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vc32,vm32 -> mess:tuple3(bt(b0[]),h(h(u0[],slbA[]),fpc[]),false[]),vc32,vm32; (* assignment on l.84 *) mess:tuple3(b0[],h(u1[],v3),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vc32,vm32 -> mess:tuple3(bt(b0[]),h(h(u0[],slbA[]),fpc[]),false[]),vc32,vm32; (* assignment on l.84 *) mess:tuple3(b0[],h(h(u1[],v3),v4),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vc32,vm32 -> mess:tuple3(bt(b0[]),h(h(u0[],slbA[]),fpc[]),false[]),vc32,vm32; (* assignment on l.84 *) mess:tuple3(b0[],u0[],false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb & att:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vm32 -> att:tuple3(bt(b0[]),h(h(u0[],slbA[]),fpc[]),false[]),vm32; (* assignment on l.84 *) mess:tuple3(b0[],h(u0[],v1),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb & att:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vm32 -> att:tuple3(bt(b0[]),h(h(u0[],slbA[]),fpc[]),false[]),vm32; (* assignment on l.84 *) mess:tuple3(b0[],h(h(u0[],v1),v2),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb & att:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vm32 -> att:tuple3(bt(b0[]),h(h(u0[],slbA[]),fpc[]),false[]),vm32; (* assignment on l.84 *) mess:tuple3(b0[],u1[],false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb & att:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vm32 -> att:tuple3(bt(b0[]),h(h(u0[],slbA[]),fpc[]),false[]),vm32; (* assignment on l.84 *) mess:tuple3(b0[],h(u1[],v3),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb & att:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vm32 -> att:tuple3(bt(b0[]),h(h(u0[],slbA[]),fpc[]),false[]),vm32; (* assignment on l.84 *) mess:tuple3(b0[],h(h(u1[],v3),v4),false[]),vc10,vm10 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],aenc(pk(xsk_Slb),y_24,tuple2(xPwd,y_25)) & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSalt & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],xSdata & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),c[],y_25 & mess:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),loc2priv[],xsk_Slb & att:tuple3(bt(b0[]),h(u0[],slbA[]),true[]),vm32 -> att:tuple3(bt(b0[]),h(h(u0[],slbA[]),fpc[]),false[]),vm32; (* assignment on l.84 *) mess:tuple3(xBoot,u0[],xFlag),c[],xNonce -> mess:tuple3(b0[],u1[],false[]),c[],aenc(pk(skSlb'3[]),r'8[],tuple2(pwd'4[],xNonce)); (* output on l.46 *) mess:tuple3(xBoot,h(u0[],v1),xFlag),c[],xNonce -> mess:tuple3(b0[],u1[],false[]),c[],aenc(pk(skSlb'3[]),r'8[],tuple2(pwd'4[],xNonce)); (* output on l.46 *) mess:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),c[],xNonce -> mess:tuple3(b0[],u1[],false[]),c[],aenc(pk(skSlb'3[]),r'8[],tuple2(pwd'4[],xNonce)); (* output on l.46 *) mess:tuple3(xBoot,u1[],xFlag),c[],xNonce -> mess:tuple3(b0[],u1[],false[]),c[],aenc(pk(skSlb'3[]),r'8[],tuple2(pwd'4[],xNonce)); (* output on l.46 *) mess:tuple3(xBoot,h(u1[],v3),xFlag),c[],xNonce -> mess:tuple3(b0[],u1[],false[]),c[],aenc(pk(skSlb'3[]),r'8[],tuple2(pwd'4[],xNonce)); (* output on l.46 *) mess:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),c[],xNonce -> mess:tuple3(b0[],u1[],false[]),c[],aenc(pk(skSlb'3[]),r'8[],tuple2(pwd'4[],xNonce)); (* output on l.46 *) mess:tuple3(xBoot,u0[],xFlag),c[],md5(tuple2(salt'5[],pwd'4[])) -> mess:tuple3(b0[],u1[],false[]),c[],allow_login[]; (* output on l.53 *) mess:tuple3(xBoot,h(u0[],v1),xFlag),c[],md5(tuple2(salt'5[],pwd'4[])) -> mess:tuple3(b0[],u1[],false[]),c[],allow_login[]; (* output on l.53 *) mess:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),c[],md5(tuple2(salt'5[],pwd'4[])) -> mess:tuple3(b0[],u1[],false[]),c[],allow_login[]; (* output on l.53 *) mess:tuple3(xBoot,u1[],xFlag),c[],md5(tuple2(salt'5[],pwd'4[])) -> mess:tuple3(b0[],u1[],false[]),c[],allow_login[]; (* output on l.53 *) mess:tuple3(xBoot,h(u1[],v3),xFlag),c[],md5(tuple2(salt'5[],pwd'4[])) -> mess:tuple3(b0[],u1[],false[]),c[],allow_login[]; (* output on l.53 *) mess:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),c[],md5(tuple2(salt'5[],pwd'4[])) -> mess:tuple3(b0[],u1[],false[]),c[],allow_login[]; (* output on l.53 *) mess:tuple3(xBoot,u0[],xFlag),c[],aenc(pk(skSlb'3[]),y_13,tuple2(xPwd,y_14)) & mess:tuple3(xBoot,u0[],xFlag),c[],xSalt & mess:tuple3(xBoot,u0[],xFlag),c[],y_14 -> mess:tuple3(b0[],u1[],false[]),c[],md5(tuple2(xSalt,xPwd)); (* output on l.98 *) mess:tuple3(xBoot,h(u0[],v1),xFlag),c[],aenc(pk(skSlb'3[]),y_13,tuple2(xPwd,y_14)) & mess:tuple3(xBoot,h(u0[],v1),xFlag),c[],xSalt & mess:tuple3(xBoot,h(u0[],v1),xFlag),c[],y_14 -> mess:tuple3(b0[],u1[],false[]),c[],md5(tuple2(xSalt,xPwd)); (* output on l.98 *) mess:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),c[],aenc(pk(skSlb'3[]),y_13,tuple2(xPwd,y_14)) & mess:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),c[],xSalt & mess:tuple3(xBoot,h(h(u0[],v1),v2),xFlag),c[],y_14 -> mess:tuple3(b0[],u1[],false[]),c[],md5(tuple2(xSalt,xPwd)); (* output on l.98 *) mess:tuple3(xBoot,u1[],xFlag),c[],aenc(pk(skSlb'3[]),y_13,tuple2(xPwd,y_14)) & mess:tuple3(xBoot,u1[],xFlag),c[],xSalt & mess:tuple3(xBoot,u1[],xFlag),c[],y_14 -> mess:tuple3(b0[],u1[],false[]),c[],md5(tuple2(xSalt,xPwd)); (* output on l.98 *) mess:tuple3(xBoot,h(u1[],v3),xFlag),c[],aenc(pk(skSlb'3[]),y_13,tuple2(xPwd,y_14)) & mess:tuple3(xBoot,h(u1[],v3),xFlag),c[],xSalt & mess:tuple3(xBoot,h(u1[],v3),xFlag),c[],y_14 -> mess:tuple3(b0[],u1[],false[]),c[],md5(tuple2(xSalt,xPwd)); (* output on l.98 *) mess:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),c[],aenc(pk(skSlb'3[]),y_13,tuple2(xPwd,y_14)) & mess:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),c[],xSalt & mess:tuple3(xBoot,h(h(u1[],v3),v4),xFlag),c[],y_14 -> mess:tuple3(b0[],u1[],false[]),c[],md5(tuple2(xSalt,xPwd)). (* output on l.98 *)