--------------------------------------------------------------
Verification summary:

Query not (event(ServerID(idS,gxy_2)) && event(ClientID(idXS,gxy_2))) is false.

Query not event(Accepted(ev)) is false.

Query not event(Appraised(log)) is false.

Query not event(ClientConn(ev)) is false.

Query not event(ClientFinished(pubAK_6,psk_2,cr_2,sr_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2)) is false.

Query not event(ClientFinRecentAgr(ID_S_2,ID_C_3,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2,cr_2,sr_2)) is false.

Query not event(ServerFinished(cr_2,sr_2,psk_2,pubLTK_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2)) is false.

Query not event(AcceptedRdata(rdata_2)) is false.

Query event(ClientFinished(pubEK_5,psk_2,cr_2,sr_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2)) && event(ServerFinished(cr_2,sr_2,psk_2,pubLTK_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2)) ==> event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(SentBadElement) || event(LeakedAK(pubAK_6)) || event(LeakedEK(pubEK_5)) || event(CompromisedCA(pubCA_1)) || event(CompromisedCSP(pubISV_1)) is false.

Query event(ClientComp(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2,cr_2,sr_2,pubEK_5,dev_state)) && event(ServerComp(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,cr_2,sr_2,pubEK_5,dev_state)) ==> event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(SentBadElement) || event(LeakedAK(pubAK_6)) || event(LeakedEK(pubEK_5)) || event(CompromisedCA(pubCA_1)) || event(CompromisedCSP(pubISV_1)) is false.

Query not (event(ClientStateEv(ev,gxy_2)) && event(ServerStateEv(ev,gxy_2))) is false.

Query not (event(ClientStateEvKch(ev,kch_4)) && event(ServerStateEvKch(ev,kch_4))) is false.

Query not (event(ClientStateEvKc(ev,kc_4)) && event(ServerStateEvKc(ev,kc_4))) is false.

Query event(ClientStateEv(ev,gxy1)) && event(ServerStateEv(ev,gxy2)) ==> gxy1 = gxy2 is true.

Query event(ClientStateEvKch(ev,kch1)) && event(ServerStateEvKch(ev,kch2)) ==> kch1 = kch2 is true.

Query event(ClientStateEvKc(ev,kc1)) && event(ServerStateEvKc(ev,kc2)) ==> kc1 = kc2 || event(ClientID(ID,e2b(BadElement))) is true.

Query event(ClientStateEvKc(ev,kc1)) && event(ServerStateEvKc(ev,kc2)) ==> kc1 = kc2 is false.

Query event(ClientComp(ID1,pubLTK_2,psk_2,offer_2,mode_2,kc1,ks_4,ems_4,rms_2,cr_2,sr_2,pubEK_5,dev_status1_2)) && event(ClientStateEvKc(ev1,kc1)) && event(PreServerComp(ID2,pubLTK_2,psk_2,offer_2,mode_2,kc2,ks_4,ems_4,cr_2,sr_2,pubEK_5,dev_status2)) && event(ServerStateEvKc(ev2,kc2)) ==> (kc1,ev1) = (kc2,ev2) || event(ClientID(ID,e2b(BadElement))) is true.

Query event(ClientComp(ID1,pubLTK_2,psk_2,offer_2,mode_2,kc1,ks_4,ems_4,rms_2,cr_2,sr_2,pubEK_5,dev_status1_2)) && event(ClientStateEvKc(ev1,kc1)) && event(PreServerComp(ID2,pubLTK_2,psk_2,offer_2,mode_2,kc2,ks_4,ems_4,cr_2,sr_2,pubEK_5,dev_status2)) && event(ServerStateEvKc(ev2,kc2)) ==> (kc1,ev1) = (kc2,ev2) is true.

Query event(ServerID(idS,gxy_2)) && event(ClientID(idXS,gxy_2)) ==> idS = idXS || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(SentBadElement) || event(LeakedAK(pubAK_6)) is false.

Query event(ServerID(idS,gxy_2)) && event(ClientID(idXS,gxy_2)) ==> idS = idXS || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(SentBadElement) || event(LeakedAK(pubAK_6)) || event(CompromisedCSP(pubISV_1)) is true.

Query event(ServerID(idS,gxy_2)) && event(ClientID(idXS,gxy_2)) ==> idS = idXS || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(SentBadElement) || event(LeakedEK(pubEK_5)) is false.

Query event(ServerID(idS,gxy_2)) && event(ClientID(idXS,gxy_2)) ==> idS = idXS || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(SentBadElement) || event(LeakedEK(pubEK_5)) || event(CompromisedCA(pubCA_1)) is true.

Query inj-event(ClientRA(pubAK_6,pubEK_5,dev_state,ev)) ==> inj-event(ServerRA(ID,pubLTK_2,pubAK_6,pubEK_5,dev_state,ev)) || event(LeakedAK(pubAK_6)) is false.

Query inj-event(ClientRA(pubAK_6,pubEK_5,dev_state,ev)) ==> inj-event(ServerRA(ID,pubLTK_2,pubAK_6,pubEK_5,dev_state,ev)) || event(LeakedAK(pubAK_6)) || event(CompromisedCSP(pubISV_1)) is true.

Query inj-event(ClientRA(pubAK_6,pubEK_5,dev_state,ev)) ==> inj-event(ServerRA(ID,pubLTK_2,pubAK_6,pubEK_5,dev_state,ev)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(SentBadElement) || event(LeakedEK(pubEK_5)) is false.

Query inj-event(ClientRA(pubAK_6,pubEK_5,dev_state,ev)) ==> inj-event(ServerRA(ID,pubLTK_2,pubAK_6,pubEK_5,dev_state,ev)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(SentBadElement) || event(LeakedEK(pubEK_5)) || event(CompromisedCA(pubCA_1)) is true.

Query inj-event(AcceptedRdata(dev_state)) ==> inj-event(SentRdata(dev_state)) || event(LeakedAK(pubAK_6)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) is false.

Query inj-event(AcceptedRdata(dev_state)) ==> inj-event(SentRdata(dev_state)) || event(LeakedAK(pubAK_6)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(CompromisedCSP(pubISV_1)) is true.

Query inj-event(AcceptedRdata(dev_state)) ==> inj-event(SentRdata(dev_state)) || event(LeakedEK(pubEK_5)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) is false.

Query inj-event(AcceptedRdata(dev_state)) ==> inj-event(SentRdata(dev_state)) || event(LeakedEK(pubEK_5)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(CompromisedCA(pubCA_1)) is true.

Query inj-event(ClientConn(ev)) ==> inj-event(Sent(ev)) || event(LeakedAK(pubAK_6)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) is false.

Query inj-event(ClientConn(ev)) ==> inj-event(Sent(ev)) || event(LeakedAK(pubAK_6)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(CompromisedCSP(pubISV_1)) is true.

Query inj-event(ClientConn(ev)) ==> inj-event(Sent(ev)) || event(LeakedEK(pubEK_5)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) is false.

Query inj-event(ClientConn(ev)) ==> inj-event(Sent(ev)) || event(LeakedEK(pubEK_5)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(CompromisedCA(pubCA_1)) is true.

Query inj-event(ClientFinRecent1WayAgr(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2,cr_2,sr_2)) ==> inj-event(PreServerFinRecent1WayAgr(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,cr_2,sr_2)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(SentBadElement) || event(LeakedAK(pubAK_6)) is false.

Query inj-event(ClientFinRecent1WayAgr(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2,cr_2,sr_2)) ==> inj-event(PreServerFinRecent1WayAgr(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,cr_2,sr_2)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(SentBadElement) || event(LeakedAK(pubAK_6)) || event(CompromisedCSP(pubISV_1)) is true.

Query inj-event(ClientFinishedWithID(ID_S_2,pubLTK_2,pubAK_6,psk_2,cr_2,sr_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2)) ==> inj-event(PreServerFinRecent1WayAgr(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,cr_2,sr_2)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(SentBadElement) || event(LeakedAK(pubAK_6)) || event(CompromisedCSP(pubISV_1)) is true.

Query inj-event(ClientFinRecent1WayAgr(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2,cr_2,sr_2)) ==> inj-event(PreServerFinRecent1WayAgr(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,cr_2,sr_2)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(SentBadElement) || event(LeakedEK(pubEK_5)) is false.

Query inj-event(ClientFinRecent1WayAgr(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2,cr_2,sr_2)) ==> inj-event(PreServerFinRecent1WayAgr(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,cr_2,sr_2)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(SentBadElement) || event(LeakedEK(pubEK_5)) || event(CompromisedCA(pubCA_1)) is true.

Query inj-event(ClientComp(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2,cr_2,sr_2,pubEK_5,dev_state)) ==> inj-event(PreServerComp(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,cr_2,sr_2,pubEK_5,dev_state)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(LeakedAK(pubAK_6)) is false.

Query inj-event(ClientComp(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2,cr_2,sr_2,pubEK_5,dev_state)) ==> inj-event(PreServerComp(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,cr_2,sr_2,pubEK_5,dev_state)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(LeakedAK(pubAK_6)) || event(CompromisedCSP(pubISV_1)) is true.

Query inj-event(ClientComp(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2,cr_2,sr_2,pubEK_5,dev_state)) ==> inj-event(PreServerComp(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,cr_2,sr_2,pubEK_5,dev_state)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(LeakedEK(pubEK_5)) is false.

Query inj-event(ClientComp(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2,cr_2,sr_2,pubEK_5,dev_state)) ==> inj-event(PreServerComp(ID_S_2,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,cr_2,sr_2,pubEK_5,dev_state)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(LeakedEK(pubEK_5)) || event(CompromisedCA(pubCA_1)) is true.

Query not event(AttackerControlsHSK(kch_4,ksh_4)) is false.

Query not event(ClientStateEvKch(ev,kch_4)) is false.

Query not (event(AttackerControlsHSK(kch_4,ksh_4)) && event(ClientStateEvKch(ev,kch_4))) is false.

Query not (event(AttackerControlsHSK(kch_4,ksh_4)) && event(ClientStateEvKch(ev,kch_4)) && attacker(kch_4)) is false.

Query event(ClientRANew(NULL_ID,NULL_pubkey,pubAK_6,pubEK_5,dev_status1_2,ev)) && event(ClientFin1WayAgr(ID,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2)) && event(ClientStateEvKc(ev,kc_4)) && attacker(kc_4) ==> event(LeakedAK(pubAK_6)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) is false.

Query event(ClientRANew(NULL_ID,NULL_pubkey,pubAK_6,pubEK_5,dev_status1_2,ev)) && event(ClientFin1WayAgr(ID,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2)) && event(ClientStateEvKc(ev,kc_4)) && attacker(kc_4) ==> event(LeakedAK(pubAK_6)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(CompromisedCSP(pubISV_1)) is true.

Query event(ClientRANew(NULL_ID,NULL_pubkey,pubAK_6,pubEK_5,dev_status1_2,ev)) && event(ClientFin1WayAgr(ID,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2)) && event(ClientStateEvKc(ev,kc_4)) && attacker(kc_4) ==> event(LeakedEK(pubEK_5)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) is false.

Query event(ClientRANew(NULL_ID,NULL_pubkey,pubAK_6,pubEK_5,dev_status1_2,ev)) && event(ClientFin1WayAgr(ID,pubLTK_2,psk_2,offer_2,mode_2,kc_4,ks_4,ems_4,rms_2)) && event(ClientStateEvKc(ev,kc_4)) && attacker(kc_4) ==> event(LeakedEK(pubEK_5)) || event(ClientAcceptsElement(cr_2,BadElement)) || event(ClientAcceptsHash(cr_2,WeakHash)) || event(CompromisedCA(pubCA_1)) is true.

--------------------------------------------------------------