--- a/src/HOL/Auth/TLS.ML Tue Sep 16 14:40:01 1997 +0200
+++ b/src/HOL/Auth/TLS.ML Wed Sep 17 16:37:21 1997 +0200
@@ -48,47 +48,27 @@
(*Injectiveness of key-generating functions*)
-AddIffs [inj_PRF RS inj_eq, inj_clientK RS inj_eq, inj_serverK RS inj_eq];
+AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq];
-(* invKey(clientK x) = clientK x and similarly for serverK*)
-Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
- isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
+(* invKey(sessionK x) = sessionK x*)
+Addsimps [isSym_sessionK, rewrite_rule [isSymKey_def] isSym_sessionK];
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
-goal thy "pubK A ~= clientK arg";
-br notI 1;
-by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
-by (Full_simp_tac 1);
-qed "pubK_neq_clientK";
-
-goal thy "pubK A ~= serverK arg";
-br notI 1;
-by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
-by (Full_simp_tac 1);
-qed "pubK_neq_serverK";
-
-goal thy "priK A ~= clientK arg";
+goal thy "pubK A ~= sessionK arg";
br notI 1;
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
by (Full_simp_tac 1);
-qed "priK_neq_clientK";
+qed "pubK_neq_sessionK";
-goal thy "priK A ~= serverK arg";
+goal thy "priK A ~= sessionK arg";
br notI 1;
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
by (Full_simp_tac 1);
-qed "priK_neq_serverK";
+qed "priK_neq_sessionK";
-(*clientK and serverK have disjoint ranges*)
-goal thy "clientK arg ~= serverK arg'";
-by (cut_facts_tac [rangeI RS impOfSubs clientK_range] 1);
-by (Blast_tac 1);
-qed "clientK_neq_serverK";
-
-val keys_distinct = [pubK_neq_clientK, pubK_neq_serverK,
- priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK];
+val keys_distinct = [pubK_neq_sessionK, priK_neq_sessionK];
AddIffs (keys_distinct @ (keys_distinct RL [not_sym]));
@@ -263,27 +243,6 @@
qed "Notes_Crypt_parts_sees";
-(*****************
- (*NEEDED? TRUE???
- Every Nonce that's hashed is already in past traffic.
- This general formulation is tricky to prove and hard to use, since the
- 2nd premise is typically proved by simplification.*)
- goal thy "!!evs. [| Hash X : parts (sees Spy evs); \
- \ Nonce N : parts {X}; evs : tls |] \
- \ ==> Nonce N : parts (sees Spy evs)";
- by (etac rev_mp 1);
- by (parts_induct_tac 1);
- by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
- Says_imp_sees_Spy RS parts.Inj]
- addSEs partsEs) 1);
- by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
- by (Fake_parts_insert_tac 1);
- (*CertVerify, ClientFinished, ServerFinished (?)*)
- by (REPEAT (Blast_tac 1));
- qed "Hash_imp_Nonce_seen";
-****************************************************************)
-
-
(*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
(*B can check A's signature if he has received A's certificate.
@@ -326,7 +285,7 @@
by (etac tls.induct 1);
by (ALLGOALS
(asm_simp_tac (analz_image_keys_ss
- addsimps (certificate_def::keys_distinct))));
+ addsimps (analz_insert_certificate::keys_distinct))));
(*Fake*)
by (spy_analz_tac 2);
(*Base*)
@@ -341,24 +300,28 @@
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
val lemma = result();
-(*Knowing some clientKs and serverKs is no help in getting new nonces*)
+(*slightly speeds up the big simplification below*)
+goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
+by (Blast_tac 1);
+val range_sessionkeys_not_priK = result();
+
+(*Knowing some session keys is no help in getting new nonces*)
goal thy
"!!evs. evs : tls ==> \
-\ ALL KK. KK <= (range clientK Un range serverK) --> \
+\ ALL KK. KK <= range sessionK --> \
\ (Nonce N : analz (Key``KK Un (sees Spy evs))) = \
\ (Nonce N : analz (sees Spy evs))";
by (etac tls.induct 1);
by (ClientCertKeyEx_tac 6);
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac lemma));
-writeln"SLOW simplification: 60 secs!??";
+writeln"SLOW simplification: 55 secs??";
+(*ClientCertKeyEx is to blame, causing case splits for A, B: lost*)
by (ALLGOALS
(asm_simp_tac (analz_image_keys_ss
- addsimps (analz_image_priK::certificate_def::
- keys_distinct))));
+ addsimps [range_sessionkeys_not_priK,
+ analz_image_priK, analz_insert_certificate])));
by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
-(*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
-by (Blast_tac 3);
(*Fake*)
by (spy_analz_tac 2);
(*Base*)
@@ -374,29 +337,6 @@
Addsimps [no_Notes_A_PRF];
-(*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
-goal thy
- "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
-\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
-\ Nonce PMS ~: analz (sees Spy evs)";
-by (analz_induct_tac 1); (*47 seconds???*)
-(*ClientHello*)
-by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
- addSEs sees_Spy_partsEs) 3);
-(*SpyKeys*)
-by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
-by (fast_tac (!claset addss (!simpset)) 2);
-(*Fake*)
-by (spy_analz_tac 1);
-(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
-by (REPEAT (blast_tac (!claset addSEs partsEs
- addDs [Notes_Crypt_parts_sees,
- impOfSubs analz_subset_parts,
- Says_imp_sees_Spy RS analz.Inj]) 1));
-bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
-
-
-
goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (sees Spy evs); \
\ evs : tls |] \
\ ==> Nonce PMS : parts (sees Spy evs)";
@@ -404,54 +344,24 @@
by (parts_induct_tac 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
by (Fake_parts_insert_tac 1);
-(*Client key exchange*)
-by (Blast_tac 4);
-(*Server Hello: by freshness*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
-(*Client Hello: trivial*)
-by (Blast_tac 2);
-(*SpyKeys*)
-by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
+(*Six others, all trivial or by freshness*)
+by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
+ addSEs sees_Spy_partsEs) 1));
qed "MS_imp_PMS";
AddSDs [MS_imp_PMS];
-(*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
- will stay secret.*)
-goal thy
- "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
-\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
-\ Nonce (PRF(PMS,NA,NB)) ~: analz (sees Spy evs)";
-by (analz_induct_tac 1); (*47 seconds???*)
-(*ClientHello*)
-by (Blast_tac 3);
-(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
-by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
-by (blast_tac (!claset addSDs [Spy_not_see_PMS,
- Says_imp_sees_Spy RS analz.Inj]) 2);
-(*Fake*)
-by (spy_analz_tac 1);
-(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
-by (REPEAT (blast_tac (!claset addSEs partsEs
- addDs [MS_imp_PMS,
- Notes_Crypt_parts_sees,
- impOfSubs analz_subset_parts,
- Says_imp_sees_Spy RS analz.Inj]) 1));
-bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
-
-
(*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
-(** First, some lemmas about those write keys. The proofs for serverK are
- nearly identical to those for clientK. **)
+(** Some lemmas about session keys, comprising clientK and serverK **)
(*Lemma: those write keys are never sent if M (MASTER SECRET) is secure.
Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
goal thy
"!!evs. [| Nonce M ~: analz (sees Spy evs); evs : tls |] \
-\ ==> Key (clientK(NA,NB,M)) ~: parts (sees Spy evs)";
+\ ==> Key (sessionK(b,NA,NB,M)) ~: parts (sees Spy evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*SpyKeys*)
@@ -461,66 +371,35 @@
by (spy_analz_tac 2);
(*Base*)
by (Blast_tac 1);
-qed "clientK_notin_parts";
-bind_thm ("clientK_in_partsE", clientK_notin_parts RSN (2, rev_notE));
-Addsimps [clientK_notin_parts];
-AddSEs [clientK_in_partsE,
- impOfSubs analz_subset_parts RS clientK_in_partsE];
+qed "sessionK_notin_parts";
+bind_thm ("sessionK_in_partsE", sessionK_notin_parts RSN (2, rev_notE));
-goal thy
- "!!evs. [| Nonce M ~: analz (sees Spy evs); evs : tls |] \
-\ ==> Key (serverK(NA,NB,M)) ~: parts (sees Spy evs)";
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*SpyKeys*)
-by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
-by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]) 3);
-(*Fake*)
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
-qed "serverK_notin_parts";
-bind_thm ("serverK_in_partsE", serverK_notin_parts RSN (2, rev_notE));
-Addsimps [serverK_notin_parts];
-AddSEs [serverK_in_partsE,
- impOfSubs analz_subset_parts RS serverK_in_partsE];
+Addsimps [sessionK_notin_parts];
+AddSEs [sessionK_in_partsE,
+ impOfSubs analz_subset_parts RS sessionK_in_partsE];
-(*Lemma: those write keys are never used if PMS is fresh.
+(*Lemma: session keys are never used if PMS is fresh.
Nonces don't have to agree, allowing session resumption.
Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
They are NOT suitable as safe elim rules.*)
goal thy
- "!!evs. [| Nonce PMS ~: used evs; evs : tls |] \
-\ ==> Crypt (clientK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
+ "!!evs. [| Nonce PMS ~: parts (sees Spy evs); evs : tls |] \
+\ ==> Crypt (sessionK(b, Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
by (etac rev_mp 1);
by (analz_induct_tac 1);
-(*ClientFinished: since M is fresh, a different instance of clientK was used.*)
-by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
- addSEs sees_Spy_partsEs) 3);
+(*Fake*)
+by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2);
by (Fake_parts_insert_tac 2);
-(*Base*)
-by (Blast_tac 1);
-qed "Crypt_clientK_notin_parts";
-Addsimps [Crypt_clientK_notin_parts];
-AddEs [Crypt_clientK_notin_parts RSN (2, rev_notE)];
+(*Base, ClientFinished, ServerFinished: trivial, e.g. by freshness*)
+by (REPEAT
+ (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
+ addSEs sees_Spy_partsEs) 1));
+qed "Crypt_sessionK_notin_parts";
-goal thy
- "!!evs. [| Nonce PMS ~: used evs; evs : tls |] \
-\ ==> Crypt (serverK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
-by (etac rev_mp 1);
-by (analz_induct_tac 1);
-(*ServerFinished: since M is fresh, a different instance of serverK was used.*)
-by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
- addSEs sees_Spy_partsEs) 3);
-by (Fake_parts_insert_tac 2);
-(*Base*)
-by (Blast_tac 1);
-qed "Crypt_serverK_notin_parts";
-
-Addsimps [Crypt_serverK_notin_parts];
-AddEs [Crypt_serverK_notin_parts RSN (2, rev_notE)];
+Addsimps [Crypt_sessionK_notin_parts];
+AddEs [Crypt_sessionK_notin_parts RSN (2, rev_notE)];
(*NEEDED??*)
@@ -559,7 +438,7 @@
qed "unique_PMS";
-(*In A's note to herself, PMS determines A and B.*)
+(*In A's internal Note, PMS determines A and B.*)
goal thy
"!!evs. [| Nonce PMS ~: analz (sees Spy evs); evs : tls |] \
\ ==> EX A' B'. ALL A B. \
@@ -583,6 +462,60 @@
+(*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
+goal thy
+ "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
+\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\ Nonce PMS ~: analz (sees Spy evs)";
+by (analz_induct_tac 1); (*30 seconds???*)
+(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
+by (REPEAT (fast_tac (!claset addss (!simpset)) 6));
+(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
+by (REPEAT (blast_tac (!claset addSEs partsEs
+ addDs [Notes_Crypt_parts_sees,
+ impOfSubs analz_subset_parts,
+ Says_imp_sees_Spy RS analz.Inj]) 4));
+(*ClientHello*)
+by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
+ addSEs sees_Spy_partsEs) 3);
+(*SpyKeys*)
+by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
+by (fast_tac (!claset addss (!simpset)) 2);
+(*Fake*)
+by (spy_analz_tac 1);
+bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
+
+
+
+
+
+(*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
+ will stay secret.*)
+goal thy
+ "!!evs. [| evs : tls; A ~: lost; B ~: lost |] \
+\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
+\ Nonce (PRF(PMS,NA,NB)) ~: analz (sees Spy evs)";
+by (analz_induct_tac 1); (*35 seconds*)
+(*ClientAccepts and ServerAccepts: because PMS was already visible*)
+by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS,
+ Says_imp_sees_Spy RS analz.Inj,
+ Notes_imp_sees_Spy RS analz.Inj]) 6));
+(*ClientHello*)
+by (Blast_tac 3);
+(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
+by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
+by (blast_tac (!claset addSDs [Spy_not_see_PMS,
+ Says_imp_sees_Spy RS analz.Inj]) 2);
+(*Fake*)
+by (spy_analz_tac 1);
+(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
+by (REPEAT (blast_tac (!claset addSEs partsEs
+ addDs [Notes_Crypt_parts_sees,
+ impOfSubs analz_subset_parts,
+ Says_imp_sees_Spy RS analz.Inj]) 1));
+bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
+
+
(*** Protocol goals: if A receives SERVER FINISHED, then B is present
and has used the quoted values XA, XB, etc. Note that it is up to A
to compare XA with what she originally sent.
@@ -599,11 +532,12 @@
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ X : parts (sees Spy evs) --> Says B A X : set evs";
by (hyp_subst_tac 1);
-by (analz_induct_tac 1);
+by (analz_induct_tac 1); (*16 seconds*)
+(*ClientCertKeyEx*)
+by (Blast_tac 2);
(*Fake: the Spy doesn't have the critical session key!*)
by (REPEAT (rtac impI 1));
-by (subgoal_tac
- "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
+by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(sees Spy evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
@@ -622,11 +556,12 @@
\ Crypt (serverK(Na,Nb,M)) Y : parts (sees Spy evs) --> \
\ (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
by (hyp_subst_tac 1);
-by (analz_induct_tac 1);
+by (analz_induct_tac 1); (*12 seconds*)
by (REPEAT_FIRST (rtac impI));
+(*ClientCertKeyEx*)
+by (Blast_tac 2);
(*Fake: the Spy doesn't have the critical session key!*)
-by (subgoal_tac
- "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
+by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(sees Spy evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
@@ -635,7 +570,7 @@
(*...otherwise delete induction hyp and use unicity of PMS.*)
by (thin_tac "?PP-->?QQ" 1);
by (Step_tac 1);
-by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsSF)" 1);
+by (subgoal_tac "Nonce PMS ~: analz(sees Spy evsSF)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
by (blast_tac (!claset addSEs [MPair_parts]
addDs [Notes_Crypt_parts_sees,
@@ -654,11 +589,12 @@
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (sees Spy evs) --> \
\ Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
-by (analz_induct_tac 1);
+by (analz_induct_tac 1); (*13 seconds*)
by (REPEAT_FIRST (rtac impI));
+(*ClientCertKeyEx*)
+by (Blast_tac 2);
(*Fake: the Spy doesn't have the critical session key!*)
-by (subgoal_tac
- "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
+by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(sees Spy evsa)" 1);
by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS,
not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
--- a/src/HOL/Auth/TLS.thy Tue Sep 16 14:40:01 1997 +0200
+++ b/src/HOL/Auth/TLS.thy Wed Sep 17 16:37:21 1997 +0200
@@ -41,8 +41,10 @@
(*Pseudo-random function of Section 5*)
PRF :: "nat*nat*nat => nat"
- (*Client, server write keys implicitly include the MAC secrets.*)
- clientK, serverK :: "nat*nat*nat => key"
+ (*Client, server write keys generated uniformly by function sessionK
+ to avoid duplicating their properties.
+ Theyimplicitly include the MAC secrets.*)
+ sessionK :: "bool*nat*nat*nat => key"
certificate :: "[agent,key] => msg"
@@ -50,16 +52,24 @@
certificate_def
"certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
+syntax
+ clientK, serverK :: "nat*nat*nat => key"
+
+translations
+ "clientK x" == "sessionK(True,x)"
+ "serverK x" == "sessionK(False,x)"
+
rules
inj_PRF "inj PRF"
- (*clientK is collision-free and makes symmetric keys*)
- inj_clientK "inj clientK"
- isSym_clientK "isSymKey (clientK x)" (*client write keys are symmetric*)
+ (*sessionK is collision-free and makes symmetric keys*)
+ inj_sessionK "inj sessionK"
+
+ isSym_sessionK "isSymKey (sessionK x)"
(*serverK is similar*)
inj_serverK "inj serverK"
- isSym_serverK "isSymKey (serverK x)" (*server write keys are symmetric*)
+ isSym_serverK "isSymKey (serverK x)"
(*Clashes with pubK and priK are impossible, but this axiom is needed.*)
clientK_range "range clientK <= Compl (range serverK)"
@@ -179,6 +189,37 @@
Nonce NB, Number XB, Agent B|}))
# evsSF : tls"
+ (*Having transmitted CLIENT FINISHED and received an identical
+ message encrypted with serverK, the client stores the parameters
+ needed to resume this session.*)
+ ClientAccepts
+ "[| evsCA: tls;
+ Notes A {|Agent B, Nonce PMS|} : set evsCA;
+ M = PRF(PMS,NA,NB);
+ X = Hash{|Nonce M, Number SID,
+ Nonce NA, Number XA, Agent A,
+ Nonce NB, Number XB, Agent B|};
+ Says A B (Crypt (clientK(NA,NB,M)) X) : set evsCA;
+ Says B' A (Crypt (serverK(NA,NB,M)) X) : set evsCA |]
+ ==>
+ Notes A {|Number SID, Agent A, Agent B, Nonce M|} # evsCA : tls"
+
+ (*Having transmitted SERVER FINISHED and received an identical
+ message encrypted with clientK, the server stores the parameters
+ needed to resume this session.*)
+ ServerAccepts
+ "[| evsSA: tls;
+ Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
+ : set evsSA;
+ M = PRF(PMS,NA,NB);
+ X = Hash{|Nonce M, Number SID,
+ Nonce NA, Number XA, Agent A,
+ Nonce NB, Number XB, Agent B|};
+ Says B A (Crypt (serverK(NA,NB,M)) X) : set evsSA;
+ Says A' B (Crypt (clientK(NA,NB,M)) X) : set evsSA |]
+ ==>
+ Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA : tls"
+
(**Oops message??**)
end