Skip to content

Commit

Permalink
cleanup: make PKI more aware of PrivateKeys (#65)
Browse files Browse the repository at this point in the history
* cleanup: make PrivateKeys more aware of PKI

* re-center around PrivateKeys

* `public_key_type` -> `long_term_key_type`

* fix CI
  • Loading branch information
TWal authored Oct 15, 2024
1 parent e2411d6 commit 0a6a843
Show file tree
Hide file tree
Showing 11 changed files with 129 additions and 109 deletions.
18 changes: 9 additions & 9 deletions examples/iso_dh/DY.Example.DH.Debug.fst
Original file line number Diff line number Diff line change
Expand Up @@ -13,27 +13,27 @@ let debug () : traceful (option unit) =

// Generate private key for Alice
let* alice_global_session_priv_key_id = initialize_private_keys alice in
generate_private_key alice alice_global_session_priv_key_id (Sign "DH.SigningKey");*
generate_private_key alice alice_global_session_priv_key_id (LongTermSigKey "DH.SigningKey");*

// Generate private key for Bob
let* bob_global_session_priv_key_id = initialize_private_keys bob in
generate_private_key bob bob_global_session_priv_key_id (Sign "DH.SigningKey");*
generate_private_key bob bob_global_session_priv_key_id (LongTermSigKey "DH.SigningKey");*

// Store Bob's public key in Alice's state
// 1. Retrieve Bob's private key from his session
// 2. Compute the public key from the private key
// 3. Initialize Alice's session to store public keys
// 4. Install Bob's public key in Alice's public key store
let*? priv_key_bob = get_private_key bob bob_global_session_priv_key_id (Sign "DH.SigningKey") in
let pub_key_bob = vk priv_key_bob in
let*? priv_key_bob = get_private_key bob bob_global_session_priv_key_id (LongTermSigKey "DH.SigningKey") in
let*? pub_key_bob = compute_public_key bob bob_global_session_priv_key_id (LongTermSigKey "DH.SigningKey") in
let* alice_global_session_pub_key_id = initialize_pki alice in
install_public_key alice alice_global_session_pub_key_id (Verify "DH.SigningKey") bob pub_key_bob;*
install_public_key alice alice_global_session_pub_key_id (LongTermSigKey "DH.SigningKey") bob pub_key_bob;*

// Store Alice's public key in Bob's state
let*? priv_key_alice = get_private_key alice alice_global_session_priv_key_id (Sign "DH.SigningKey") in
let pub_key_alice = vk priv_key_alice in
let*? priv_key_alice = get_private_key alice alice_global_session_priv_key_id (LongTermSigKey "DH.SigningKey") in
let*? pub_key_alice = compute_public_key alice alice_global_session_priv_key_id (LongTermSigKey "DH.SigningKey") in
let* bob_global_session_pub_key_id = initialize_pki bob in
install_public_key bob bob_global_session_pub_key_id (Verify "DH.SigningKey") alice pub_key_alice;*
install_public_key bob bob_global_session_pub_key_id (LongTermSigKey "DH.SigningKey") alice pub_key_alice;*

let alice_global_session_ids: dh_global_sess_ids = {pki=alice_global_session_pub_key_id; private_keys=alice_global_session_priv_key_id} in
let bob_global_session_ids: dh_global_sess_ids = {pki=bob_global_session_pub_key_id; private_keys=bob_global_session_priv_key_id} in
Expand Down Expand Up @@ -64,4 +64,4 @@ let debug () : traceful (option unit) =
//Run ``debug ()`` when the module loads
#push-options "--warn_error -272"
let _ = debug () Nil
#pop-options
#pop-options
8 changes: 4 additions & 4 deletions examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst
Original file line number Diff line number Diff line change
Expand Up @@ -212,7 +212,7 @@ val send_msg2_proof:
let send_msg2_proof tr global_sess_id bob bob_si =
match get_state bob bob_si tr with
| (Some (ResponderSentMsg2 alice gx gy y), tr) -> (
match get_private_key bob global_sess_id.private_keys (Sign "DH.SigningKey") tr with
match get_private_key bob global_sess_id.private_keys (LongTermSigKey "DH.SigningKey") tr with
| (Some sk_b, tr) -> (
let (n_sig, tr) = mk_rand SigNonce (principal_label bob) 32 tr in
compute_message2_proof tr alice bob gx y sk_b n_sig
Expand All @@ -238,7 +238,7 @@ let prepare_msg3_proof tr global_sess_id alice alice_si bob msg_id =
| (Some (InitiatorSentMsg1 bob x), tr) -> (
match recv_msg msg_id tr with
| (Some msg_bytes, tr) -> (
match get_public_key alice global_sess_id.pki (Verify "DH.SigningKey") bob tr with
match get_public_key alice global_sess_id.pki (LongTermSigKey "DH.SigningKey") bob tr with
| (Some pk_b, tr) -> (
match decode_and_verify_message2 msg_bytes alice x pk_b with
| Some res -> (
Expand Down Expand Up @@ -301,7 +301,7 @@ val send_msg3_proof:
let send_msg3_proof tr global_sess_id alice alice_si bob =
match get_state alice alice_si tr with
| (Some (InitiatorSendMsg3 bob gx gy k), tr') -> (
match get_private_key alice global_sess_id.private_keys (Sign "DH.SigningKey") tr' with
match get_private_key alice global_sess_id.private_keys (LongTermSigKey "DH.SigningKey") tr' with
| (Some sk_a, tr') -> (
let (n_sig, tr') = mk_rand SigNonce (principal_label alice) 32 tr' in

Expand Down Expand Up @@ -336,7 +336,7 @@ let verify_msg3_proof tr global_sess_id alice bob msg_id bob_si =
| (Some (ResponderSentMsg2 alice gx gy y), tr) -> (
match recv_msg msg_id tr with
| (Some msg_bytes, tr) -> (
match get_public_key bob global_sess_id.pki (Verify "DH.SigningKey") alice tr with
match get_public_key bob global_sess_id.pki (LongTermSigKey "DH.SigningKey") alice tr with
| (Some pk_a, tr) -> (
decode_and_verify_message3_proof tr msg_bytes alice bob bob_si gx y pk_a;

Expand Down
8 changes: 4 additions & 4 deletions examples/iso_dh/DY.Example.DH.Protocol.Stateful.fst
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ let send_msg2 global_sess_id bob bob_si =
let*? session_state = get_state bob bob_si in
guard_tr (ResponderSentMsg2? session_state);*?
let ResponderSentMsg2 alice gx gy y = session_state in
let*? sk_b = get_private_key bob global_sess_id.private_keys (Sign "DH.SigningKey") in
let*? sk_b = get_private_key bob global_sess_id.private_keys (LongTermSigKey "DH.SigningKey") in
let* n_sig = mk_rand SigNonce (principal_label bob) 32 in
let msg = compute_message2 alice bob gx gy sk_b n_sig in
let* msg_id = send_msg msg in
Expand All @@ -105,7 +105,7 @@ let prepare_msg3 global_sess_id alice alice_si bob msg_id =
let*? session_state = get_state alice alice_si in
guard_tr (InitiatorSentMsg1? session_state);*?
let InitiatorSentMsg1 bob x = session_state in
let*? pk_b = get_public_key alice global_sess_id.pki (Verify "DH.SigningKey") bob in
let*? pk_b = get_public_key alice global_sess_id.pki (LongTermSigKey "DH.SigningKey") bob in
let*? msg = recv_msg msg_id in
let*? res:verify_msg2_result = return (decode_and_verify_message2 msg alice x pk_b) in
trigger_event alice (Initiate2 alice bob res.gx res.gy res.k);*
Expand All @@ -118,7 +118,7 @@ let send_msg3 global_sess_id alice bob alice_si =
let*? session_state = get_state alice alice_si in
guard_tr (InitiatorSendMsg3? session_state);*?
let InitiatorSendMsg3 bob gx gy x = session_state in
let*? sk_a = get_private_key alice global_sess_id.private_keys (Sign "DH.SigningKey") in
let*? sk_a = get_private_key alice global_sess_id.private_keys (LongTermSigKey "DH.SigningKey") in
let* n_sig = mk_rand SigNonce (principal_label alice) 32 in
let msg = compute_message3 alice bob gx gy sk_a n_sig in
let* msg_id = send_msg msg in
Expand All @@ -130,7 +130,7 @@ let verify_msg3 global_sess_id alice bob msg_id bob_si =
let*? session_state = get_state bob bob_si in
guard_tr (ResponderSentMsg2? session_state);*?
let ResponderSentMsg2 alice gx gy y = session_state in
let*? pk_a = get_public_key bob global_sess_id.pki (Verify "DH.SigningKey") alice in
let*? pk_a = get_public_key bob global_sess_id.pki (LongTermSigKey "DH.SigningKey") alice in
let*? msg = recv_msg msg_id in
let*? res:verify_msg3_result = return (decode_and_verify_message3 msg bob gx gy y pk_a) in
trigger_event bob (Respond2 alice bob gx gy res.k);*
Expand Down
10 changes: 5 additions & 5 deletions examples/iso_dh/DY.Example.DH.Protocol.Total.Proof.fst
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ val compute_message2_proof:
event_triggered tr bob (Respond1 alice bob gx (dh_pk y) y) /\
is_publishable tr gx /\
bytes_invariant tr y /\
is_signature_key (SigKey "DH.SigningKey" empty) (principal_label bob) tr sk_b /\
is_private_key_for tr sk_b (LongTermSigKey "DH.SigningKey") bob /\
is_secret (principal_label bob) tr n_sig /\
SigNonce? (get_usage n_sig)
)
Expand Down Expand Up @@ -175,7 +175,7 @@ val decode_and_verify_message2_proof:
(requires
is_publishable tr msg2_bytes /\
is_secret (principal_state_label alice alice_si) tr x /\
is_verification_key (SigKey "DH.SigningKey" empty) (principal_label bob) tr pk_b
is_public_key_for tr pk_b (LongTermSigKey "DH.SigningKey") bob
)
(ensures (
match decode_and_verify_message2 msg2_bytes alice x pk_b with
Expand Down Expand Up @@ -218,7 +218,7 @@ val compute_message3_proof:
event_triggered tr alice (Initiate2 alice bob (dh_pk x) gy (dh x gy)) /\
is_publishable tr gx /\ is_publishable tr gy /\
gx = dh_pk x /\
is_signature_key (SigKey "DH.SigningKey" empty) (principal_label alice) tr sk_a /\
is_private_key_for tr sk_a (LongTermSigKey "DH.SigningKey") alice /\
is_secret (principal_label alice) tr n_sig /\
SigNonce? (get_usage n_sig)
)
Expand Down Expand Up @@ -248,7 +248,7 @@ let compute_message3_proof tr alice bob gx gy x sk_a n_sig =
assert(is_publishable tr (serialize message msg));
()

#push-options "--ifuel 1 --z3rlimit 10"
#push-options "--ifuel 1 --z3rlimit 25"
val decode_and_verify_message3_proof:
tr:trace ->
msg3_bytes:bytes ->
Expand All @@ -259,7 +259,7 @@ val decode_and_verify_message3_proof:
is_publishable tr msg3_bytes /\
is_publishable tr gx /\
is_secret (principal_state_label bob bob_si) tr y /\
is_verification_key (SigKey "DH.SigningKey" empty) (principal_label alice) tr pk_a
is_public_key_for tr pk_a (LongTermSigKey "DH.SigningKey") alice
)
(ensures (
let gy = dh_pk y in
Expand Down
16 changes: 8 additions & 8 deletions examples/nsl_pk/DY.Example.NSL.Debug.fst
Original file line number Diff line number Diff line change
Expand Up @@ -17,27 +17,27 @@ let debug () : traceful (option unit) =

// Generate private key for Alice
let* alice_global_session_priv_key_id = initialize_private_keys alice in
generate_private_key alice alice_global_session_priv_key_id (PkDec "NSL.PublicKey");*
generate_private_key alice alice_global_session_priv_key_id (LongTermPkEncKey "NSL.PublicKey");*

// Generate private key for Bob
let* bob_global_session_priv_key_id = initialize_private_keys bob in
generate_private_key bob bob_global_session_priv_key_id (PkDec "NSL.PublicKey");*
generate_private_key bob bob_global_session_priv_key_id (LongTermPkEncKey "NSL.PublicKey");*

// Store Bob's public key in Alice's state
// 1. Retrieve Bob's private key from his session
// 2. Compute the public key from the private key
// 3. Initialize Alice's session to store public keys
// 4. Install Bob's public key in Alice's public key store
let*? priv_key_bob = get_private_key bob bob_global_session_priv_key_id (PkDec "NSL.PublicKey") in
let pub_key_bob = pk priv_key_bob in
let*? priv_key_bob = get_private_key bob bob_global_session_priv_key_id (LongTermPkEncKey "NSL.PublicKey") in
let*? pub_key_bob = compute_public_key bob bob_global_session_priv_key_id (LongTermPkEncKey "NSL.PublicKey") in
let* alice_global_session_pub_key_id = initialize_pki alice in
install_public_key alice alice_global_session_pub_key_id (PkEnc "NSL.PublicKey") bob pub_key_bob;*
install_public_key alice alice_global_session_pub_key_id (LongTermPkEncKey "NSL.PublicKey") bob pub_key_bob;*

// Store Alice's public key in Bob's state
let*? priv_key_alice = get_private_key alice alice_global_session_priv_key_id (PkDec "NSL.PublicKey") in
let pub_key_alice = pk priv_key_alice in
let*? priv_key_alice = get_private_key alice alice_global_session_priv_key_id (LongTermPkEncKey "NSL.PublicKey") in
let*? pub_key_alice = compute_public_key alice alice_global_session_priv_key_id (LongTermPkEncKey "NSL.PublicKey") in
let* bob_global_session_pub_key_id = initialize_pki bob in
install_public_key bob bob_global_session_pub_key_id (PkEnc "NSL.PublicKey") alice pub_key_alice;*
install_public_key bob bob_global_session_pub_key_id (LongTermPkEncKey "NSL.PublicKey") alice pub_key_alice;*

let alice_global_session_ids: nsl_global_sess_ids = {pki=alice_global_session_pub_key_id; private_keys=alice_global_session_priv_key_id} in
let bob_global_session_ids: nsl_global_sess_ids = {pki=bob_global_session_pub_key_id; private_keys=bob_global_session_priv_key_id} in
Expand Down
12 changes: 6 additions & 6 deletions examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,7 @@ val send_msg1_proof:
let send_msg1_proof tr global_sess_id alice sess_id =
match get_state alice sess_id tr with
| (Some (InitiatorSentMsg1 bob n_a), tr) -> (
match get_public_key alice global_sess_id.pki (PkEnc "NSL.PublicKey") bob tr with
match get_public_key alice global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") bob tr with
| (None, tr) -> ()
| (Some pk_b, tr) -> (
let (nonce, tr) = mk_rand PkNonce (principal_label alice) 32 tr in
Expand All @@ -189,7 +189,7 @@ let prepare_msg2_proof tr global_sess_id bob msg_id =
match recv_msg msg_id tr with
| (None, tr) -> ()
| (Some msg, tr) -> (
match get_private_key bob global_sess_id.private_keys (PkDec "NSL.PublicKey") tr with
match get_private_key bob global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") tr with
| (None, tr) -> ()
| (Some sk_b, tr) -> (
decode_message1_proof tr bob msg sk_b
Expand All @@ -208,7 +208,7 @@ val send_msg2_proof:
let send_msg2_proof tr global_sess_id bob sess_id =
match get_state bob sess_id tr with
| (Some (ResponderSentMsg2 alice n_a n_b), tr) -> (
match get_public_key bob global_sess_id.pki (PkEnc "NSL.PublicKey") alice tr with
match get_public_key bob global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") alice tr with
| (None, tr) -> ()
| (Some pk_a, tr) -> (
let (nonce, tr) = mk_rand PkNonce (principal_label bob) 32 tr in
Expand All @@ -230,7 +230,7 @@ let prepare_msg3_proof tr global_sess_id alice sess_id msg_id =
match recv_msg msg_id tr with
| (None, tr) -> ()
| (Some msg, tr) -> (
match get_private_key alice global_sess_id.private_keys (PkDec "NSL.PublicKey") tr with
match get_private_key alice global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") tr with
| (None, tr) -> ()
| (Some sk_a, tr) -> (
match get_state alice sess_id tr with
Expand All @@ -253,7 +253,7 @@ val send_msg3_proof:
let send_msg3_proof tr global_sess_id alice sess_id =
match get_state alice sess_id tr with
| (Some (InitiatorSentMsg3 bob n_a n_b), tr) -> (
match get_public_key alice global_sess_id.pki (PkEnc "NSL.PublicKey") bob tr with
match get_public_key alice global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") bob tr with
| (None, tr) -> ()
| (Some pk_b, tr) -> (
let (nonce, tr) = mk_rand PkNonce (principal_label alice) 32 tr in
Expand Down Expand Up @@ -292,7 +292,7 @@ let prepare_msg4 tr global_sess_id bob sess_id msg_id =
match recv_msg msg_id tr with
| (None, tr) -> ()
| (Some msg, tr) -> (
match get_private_key bob global_sess_id.private_keys (PkDec "NSL.PublicKey") tr with
match get_private_key bob global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") tr with
| (None, tr) -> ()
| (Some sk_b, tr) -> (
match get_state bob sess_id tr with
Expand Down
12 changes: 6 additions & 6 deletions examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.fst
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ let send_msg1 global_sess_id alice sess_id =
let*? st = get_state alice sess_id in
guard_tr (InitiatorSentMsg1? st);*?
let InitiatorSentMsg1 bob n_a = st in
let*? pk_b = get_public_key alice global_sess_id.pki (PkEnc "NSL.PublicKey") bob in
let*? pk_b = get_public_key alice global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") bob in
let* nonce = mk_rand PkNonce (principal_label alice) 32 in
let msg = compute_message1 alice bob pk_b n_a nonce in
let* msg_id = send_msg msg in
Expand All @@ -80,7 +80,7 @@ let send_msg1 global_sess_id alice sess_id =
val prepare_msg2: nsl_global_sess_ids -> principal -> timestamp -> traceful (option state_id)
let prepare_msg2 global_sess_id bob msg_id =
let*? msg = recv_msg msg_id in
let*? sk_b = get_private_key bob global_sess_id.private_keys (PkDec "NSL.PublicKey") in
let*? sk_b = get_private_key bob global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") in
let*? msg1: message1 = return (decode_message1 bob msg sk_b) in
let* n_b = mk_rand NoUsage (join (principal_label msg1.alice) (principal_label bob)) 32 in
trigger_event bob (Respond1 msg1.alice bob msg1.n_a n_b);*
Expand All @@ -93,7 +93,7 @@ let send_msg2 global_sess_id bob sess_id =
let*? st = get_state bob sess_id in
guard_tr (ResponderSentMsg2? st);*?
let ResponderSentMsg2 alice n_a n_b = st in
let*? pk_a = get_public_key bob global_sess_id.pki (PkEnc "NSL.PublicKey") alice in
let*? pk_a = get_public_key bob global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") alice in
let* nonce = mk_rand PkNonce (principal_label bob) 32 in
let msg = compute_message2 bob {n_a; alice;} pk_a n_b nonce in
let* msg_id = send_msg msg in
Expand All @@ -102,7 +102,7 @@ let send_msg2 global_sess_id bob sess_id =
val prepare_msg3: nsl_global_sess_ids -> principal -> state_id -> timestamp -> traceful (option unit)
let prepare_msg3 global_sess_id alice sess_id msg_id =
let*? msg = recv_msg msg_id in
let*? sk_a = get_private_key alice global_sess_id.private_keys (PkDec "NSL.PublicKey") in
let*? sk_a = get_private_key alice global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") in
let*? st = get_state alice sess_id in
guard_tr (InitiatorSentMsg1? st);*?
let InitiatorSentMsg1 bob n_a = st in
Expand All @@ -116,7 +116,7 @@ let send_msg3 global_sess_id alice sess_id =
let*? st = get_state alice sess_id in
guard_tr (InitiatorSentMsg3? st);*?
let InitiatorSentMsg3 bob n_a n_b = st in
let*? pk_b = get_public_key alice global_sess_id.pki (PkEnc "NSL.PublicKey") bob in
let*? pk_b = get_public_key alice global_sess_id.pki (LongTermPkEncKey "NSL.PublicKey") bob in
let* nonce = mk_rand PkNonce (principal_label alice) 32 in
let msg = compute_message3 alice bob pk_b n_b nonce in
let* msg_id = send_msg msg in
Expand All @@ -125,7 +125,7 @@ let send_msg3 global_sess_id alice sess_id =
val prepare_msg4: nsl_global_sess_ids -> principal -> state_id -> timestamp -> traceful (option unit)
let prepare_msg4 global_sess_id bob sess_id msg_id =
let*? msg = recv_msg msg_id in
let*? sk_b = get_private_key bob global_sess_id.private_keys (PkDec "NSL.PublicKey") in
let*? sk_b = get_private_key bob global_sess_id.private_keys (LongTermPkEncKey "NSL.PublicKey") in
let*? st = get_state bob sess_id in
guard_tr (ResponderSentMsg2? st);*?
let ResponderSentMsg2 alice n_a n_b = st in
Expand Down
12 changes: 6 additions & 6 deletions examples/nsl_pk/DY.Example.NSL.Protocol.Total.Proof.fst
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ val compute_message1_proof:
// From random generation
PkNonce? (get_usage nonce) /\
// From PKI invariants
is_encryption_key (PkKey "NSL.PublicKey" empty) (principal_label bob) tr pk_b
is_public_key_for tr pk_b (LongTermPkEncKey "NSL.PublicKey") bob
)
(ensures is_publishable tr (compute_message1 alice bob pk_b n_a nonce))
let compute_message1_proof tr alice bob pk_b n_a nonce =
Expand All @@ -93,7 +93,7 @@ val decode_message1_proof:
Lemma
(requires
// From PrivateKeys invariants
is_decryption_key (PkKey "NSL.PublicKey" empty) (principal_label bob) tr sk_b /\
is_private_key_for tr sk_b (LongTermPkEncKey "NSL.PublicKey") bob /\
// From the network
bytes_invariant tr msg_cipher
)
Expand Down Expand Up @@ -129,7 +129,7 @@ val compute_message2_proof:
// From the random generation
PkNonce? (get_usage nonce) /\
// From the PKI
is_encryption_key (PkKey "NSL.PublicKey" empty) (principal_label msg1.alice) tr pk_a
is_public_key_for tr pk_a (LongTermPkEncKey "NSL.PublicKey") msg1.alice
)
(ensures
is_publishable tr (compute_message2 bob msg1 pk_a n_b nonce)
Expand All @@ -153,7 +153,7 @@ val decode_message2_proof:
// From the NSL state invariant
is_secret (join (principal_label alice) (principal_label bob)) tr n_a /\
// From the PrivateKeys invariant
is_decryption_key (PkKey "NSL.PublicKey" empty) (principal_label alice) tr sk_a /\
is_private_key_for tr sk_a (LongTermPkEncKey "NSL.PublicKey") alice /\
// From the network
bytes_invariant tr msg_cipher
)
Expand Down Expand Up @@ -192,7 +192,7 @@ val compute_message3_proof:
// From the random generation
PkNonce? (get_usage nonce) /\
// From the PKI
is_encryption_key (PkKey "NSL.PublicKey" empty) (principal_label bob) tr pk_b
is_public_key_for tr pk_b (LongTermPkEncKey "NSL.PublicKey") bob
)
(ensures
is_publishable tr (compute_message3 alice bob pk_b n_b nonce)
Expand All @@ -217,7 +217,7 @@ val decode_message3_proof:
// From the NSL state invariant
get_label tr n_b == join (principal_label alice) (principal_label bob) /\
// From the PrivateKeys invariant
is_decryption_key (PkKey "NSL.PublicKey" empty) (principal_label bob) tr sk_b /\
is_private_key_for tr sk_b (LongTermPkEncKey "NSL.PublicKey") bob /\
// From the network
bytes_invariant tr msg_cipher
)
Expand Down
Loading

0 comments on commit 0a6a843

Please sign in to comment.