You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hardeep Kaur edited this page Nov 3, 2022
·
1 revision
let initiator_send_msg_1 a b =
print_string ("initiator "^a^" sending first message to "^b^"\n");
let si = new_session_number #tls13 a in
let (|t0,x|) = rand_gen #tls13 (readers [V a si 0]) (dh_usage "TLS13.dh_key") in
let gx = dh_pk #tls13_global_usage #t0 #(readers [V a si 0]) x in
let ev = initiate a b gx in
trigger_event #tls13 a ev;
let t1 = global_timestamp () in
let new_ss_st = InitiatorSentMsg1 b x in
let new_ss = serialize_valid_session_st t1 a si 0 new_ss_st in
new_session #(tls13) #t1 a si 0 new_ss;
let t2 = global_timestamp () in
let msg1 = Msg1 gx in
let w_msg1 = serialize_msg t2 msg1 in
let i = send #tls13 #t2 a b w_msg1 in
i,si