Require Import Notations Logic Datatypes PeanoNat String.
Local Open Scope nat_scope.
Inductive constant : Type :=
	| nil
	| value (s: string)
	| equation_c (base: constant) (exp: constant)
	| mult_c (c1: constant) (c2: constant)
	| ENC_c (key: constant) (message: constant)
	| AEAD_ENC_c (key: constant) (message: constant) (ad: constant)
	| PKE_ENC_c (G_key: constant) (message: constant)
	| CONCAT2_c (a: constant) (b: constant)
	| CONCAT3_c (a: constant) (b: constant) (c: constant)
	| CONCAT4_c (a: constant) (b: constant) (c: constant) (d: constant)
	| CONCAT5_c (a: constant) (b: constant) (c: constant) (d: constant) (e: constant)
	| HASH1_c (x: constant)
	| HASH2_c (x1: constant) (x2: constant)
	| HASH3_c (x1: constant) (x2: constant) (x3: constant)
	| HASH4_c (x1: constant) (x2: constant) (x3: constant) (x4: constant)
	| HASH5_c (x1: constant) (x2: constant) (x3: constant) (x4: constant) (x5: constant)
	| MAC_c (key: constant) (message: constant)
	| HKDF1_c (salt: constant) (ikm: constant) (info: constant)
	| HKDF2_c (salt: constant) (ikm: constant) (info: constant)
	| HKDF3_c (salt: constant) (ikm: constant) (info: constant)
	| HKDF4_c (salt: constant) (ikm: constant) (info: constant)
	| HKDF5_c (salt: constant) (ikm: constant) (info: constant)
	| PW_HASH_c (x: constant)
	| SIGN_c (k: constant) (m: constant)
	| RINGSIGN_c (key_a: constant) (G_key_b: constant) (G_key_c: constant) (message: constant)
	| SHAMIR_SPLIT1_c (k: constant)
	| SHAMIR_SPLIT2_c (k: constant)
	| SHAMIR_SPLIT3_c (k: constant)
	| SHAMIR_JOIN_c (sa: constant) (sb: constant)
	| INVALID (s: string)
	| VALID.
Definition G := value "G".
Notation "x && y" := (andb x y).
Fixpoint equal_consts(c1 c2: constant) : bool :=
	match c1, c2 with
	| nil, nil => true
	| value s1, value s2 => eqb s1 s2
	| equation_c base1 exp1, equation_c base2 exp2 => andb (equal_consts base1 base2) (equal_consts exp1 exp2)
	| mult_c a b, mult_c c d => orb (andb (equal_consts a c) (equal_consts b d)) (andb (equal_consts a d) (equal_consts b c))
	| ENC_c k1 m1, ENC_c k2 m2 => andb (equal_consts k1 k2) (equal_consts m1 m2)
	| AEAD_ENC_c k1 m1 ad1, AEAD_ENC_c k2 m2 ad2 => andb (andb (equal_consts k1 k2) (equal_consts m1 m2)) (equal_consts ad1 ad2)
	| PKE_ENC_c k1 m1, PKE_ENC_c k2 m2 => andb (equal_consts k1 k2) (equal_consts m1 m2)
	| CONCAT2_c a1 b1, CONCAT2_c a2 b2 => andb (equal_consts a1 a2) (equal_consts b1 b2)
	| CONCAT3_c a1 b1 c1, CONCAT3_c a2 b2 c2 => andb (equal_consts a1 a2) (andb (equal_consts b1 b2) (equal_consts c1 c2))
	| CONCAT4_c a1 b1 c1 d1, CONCAT4_c a2 b2 c2 d2 => andb (equal_consts a1 a2) (andb (equal_consts b1 b2) (andb(equal_consts c1 c2) (equal_consts d1 d2)))
	| CONCAT5_c a1 b1 c1 d1 e1, CONCAT5_c a2 b2 c2 d2 e2 => andb (equal_consts a1 a2) (andb (equal_consts b1 b2) (andb (equal_consts c1 c2) (andb (equal_consts d1 d2) (equal_consts e1 e2))))
	| HASH1_c a, HASH1_c b => equal_consts a b
	| HASH2_c a1 b1, HASH2_c a2 b2 => andb (equal_consts a1 a2) (equal_consts b1 b2)
	| HASH3_c a1 b1 c1, HASH3_c a2 b2 c2 => andb (equal_consts a1 a2) (andb (equal_consts b1 b2) (equal_consts c1 c2))
	| HASH4_c a1 b1 c1 d1, HASH4_c a2 b2 c2 d2 => andb (equal_consts a1 a2) (andb (equal_consts b1 b2) (andb(equal_consts c1 c2) (equal_consts d1 d2)))
	| HASH5_c a1 b1 c1 d1 e1, HASH5_c a2 b2 c2 d2 e2 => andb (equal_consts a1 a2) (andb (equal_consts b1 b2) (andb (equal_consts c1 c2) (andb (equal_consts d1 d2) (equal_consts e1 e2))))
	| MAC_c k1 m1, MAC_c k2 m2 => andb (equal_consts k1 k2) (equal_consts m1 m2)
	| PW_HASH_c a, PW_HASH_c b => equal_consts a b
	| SIGN_c k1 m1, SIGN_c k2 m2 => andb (equal_consts k1 k2) (equal_consts m1 m2)
	| RINGSIGN_c ka1 gkb1 gkc1 m1, RINGSIGN_c ka2 gkb2 gkc2 m2 => andb (andb (equal_consts ka1 ka2) (equal_consts m1 m2)) (orb (andb (equal_consts gkb1 gkb2) (equal_consts gkc1 gkc2)) (andb (equal_consts gkb1 gkc2) (equal_consts gkc1 gkb2)))
	| SHAMIR_SPLIT1_c ka, SHAMIR_SPLIT1_c kb => equal_consts ka kb
	| SHAMIR_SPLIT2_c ka, SHAMIR_SPLIT2_c kb => equal_consts ka kb
	| SHAMIR_SPLIT3_c ka, SHAMIR_SPLIT3_c kb => equal_consts ka kb
	| SHAMIR_JOIN_c sa1 sb1, SHAMIR_JOIN_c sa2 sb2 => orb (andb (equal_consts sa1 sa2)(equal_consts sb1 sb2)) (andb (equal_consts sa1 sb2) (equal_consts sb1 sa2))
	| HKDF1_c salt1 ikm1 info1, HKDF1_c salt2 ikm2 info2 => andb (equal_consts salt1 salt2) (andb (equal_consts ikm1 ikm2) (equal_consts info1 info2))
	| HKDF2_c salt1 ikm1 info1, HKDF2_c salt2 ikm2 info2 => andb (equal_consts salt1 salt2) (andb (equal_consts ikm1 ikm2) (equal_consts info1 info2))
	| HKDF3_c salt1 ikm1 info1, HKDF3_c salt2 ikm2 info2 => andb (equal_consts salt1 salt2) (andb (equal_consts ikm1 ikm2) (equal_consts info1 info2))
	| HKDF4_c salt1 ikm1 info1, HKDF4_c salt2 ikm2 info2 => andb (equal_consts salt1 salt2) (andb (equal_consts ikm1 ikm2) (equal_consts info1 info2))
	| HKDF5_c salt1 ikm1 info1, HKDF5_c salt2 ikm2 info2 => andb (equal_consts salt1 salt2) (andb (equal_consts ikm1 ikm2) (equal_consts info1 info2))
	| _, _ => false
	end.

Fixpoint multiply(c1 c2: constant) : constant :=
	match c1, c2 with
	| _, nil => c1
	| nil, _ => c2
	| _, _ => mult_c c1 c2
	end.

Notation "c1 * c2" := (multiply c1 c2) (at level 40, left associativity) : nat_scope.
(* ASSUMPTION: COMMUTATIVTY IN DH MULT*)
Theorem mult_associativity: forall b c: constant, b*c = c*b.
Admitted.

Fixpoint public_key(secret: constant) : constant := equation_c G secret.

Notation " G^( c )" := (public_key c) (at level 30, right associativity).
Notation "x =? y" := (equal_consts x y) (at level 70) : nat_scope.


Theorem pub_key: forall x: constant, public_key x = equation_c G x.
	Proof.
		intros x. destruct x eqn:E.
		reflexivity. reflexivity. reflexivity. reflexivity. reflexivity.
		reflexivity. reflexivity. reflexivity. reflexivity. reflexivity.
		reflexivity. reflexivity. reflexivity. reflexivity. reflexivity.
		reflexivity. reflexivity. reflexivity. reflexivity. reflexivity.
		reflexivity. reflexivity. reflexivity. reflexivity. reflexivity.
		reflexivity. reflexivity. reflexivity. reflexivity. reflexivity.
		reflexivity.
	Qed.

(* a private key always has the same public key *)
Theorem pub_key_eq: forall x y: constant, x = y -> public_key x = public_key y.
	Proof.
		intros x y H.
		rewrite <- H.
		reflexivity.
	Qed.

Fixpoint DH(c1 c2: constant): constant :=
	match c1, c2 with
	| equation_c base1 exp1, equation_c base2 exp2 => equation_c G (exp1 * exp2)
	| equation_c base exp, _ => equation_c G (exp * c2)
	| _, equation_c base exp => equation_c G (exp * c1)
	| _, _ => equation_c G (c1 * c2)
	end.

	(* WIP Equations *)
(* Theorem dh_eq: forall x y, (DH (public_key x) y) = equation_c G (x*y).
Proof.
intros x y.
destruct x eqn:Ex.
destruct y eqn:Ey.
reflexivity. reflexivity. simpl. reflexivity. *)
(* Theorem dh_eq: forall x y, (DH (public_key x) y) = (DH (public_key y) x). *)
(*theorem gxy = gyx*)

(* Encryption Primitives *)
Fixpoint ENC(key plaintext: constant): constant := ENC_c key plaintext.

Fixpoint DEC(key ciphertext: constant): constant :=
	match ciphertext with
	| ENC_c k m => match equal_consts k key with
				| true => m
				| false => ENC_c k m
				end
	| _ => ciphertext
	end.

(*ASSUMPTION*)
Theorem enc_dec: forall k m: constant, DEC k (ENC k m) = m.
Admitted.

Theorem enc_dec_2: forall k m c: constant, c = ENC k m -> m = DEC k c.
	Proof.
		intros k m c H.
		rewrite -> H.
		rewrite -> enc_dec.
		reflexivity.
	Qed.

Fixpoint AEAD_ENC(key plaintext ad: constant): constant := AEAD_ENC_c key plaintext ad.

Fixpoint AEAD_DEC(key ciphertext ad: constant) : constant :=
	match ciphertext with
	| AEAD_ENC_c k m ad' => match equal_consts ad ad' with
							| true => match equal_consts key k with
									| true => m
									| false => ciphertext
									end
							| false => INVALID "AEAD_DEC_fail_ad_mismatch"
							end
	| _ => ciphertext
	end.

Fixpoint PKE_ENC(gkey plaintext: constant) : constant := PKE_ENC_c gkey plaintext.

Fixpoint PKE_DEC(key ciphertext: constant) : constant :=
	match ciphertext with
	| PKE_ENC_c gkey plaintext => match equal_consts (public_key key) gkey with
								| true => plaintext
								| false => ciphertext
								end
	| _ => ciphertext
	end.

	(* Hashing Primitives *)
Fixpoint HASH1(a: constant) : constant := HASH1_c a.
Fixpoint HASH2(a: constant) (b: constant) : constant := HASH2_c a b.
Fixpoint HASH3(a: constant) (b: constant) (c: constant) : constant := HASH3_c a b c.
Fixpoint HASH4(a: constant) (b: constant) (c: constant) (d: constant) : constant := HASH4_c a b c d.
Fixpoint HASH5(a: constant) (b: constant) (c: constant) (d: constant) (e: constant) : constant := HASH5_c a b c d e.
Fixpoint MAC(key message: constant) : constant := MAC_c key message.
Fixpoint PW_HASH(a: constant) : constant := PW_HASH_c a.
Fixpoint HKDF1 (salt ikm info: constant) := HKDF1_c salt ikm info.
Fixpoint HKDF2 (salt ikm info: constant) := HKDF2_c salt ikm info.
Fixpoint HKDF3 (salt ikm info: constant) := HKDF3_c salt ikm info.
Fixpoint HKDF4 (salt ikm info: constant) := HKDF4_c salt ikm info.
Fixpoint HKDF5 (salt ikm info: constant) := HKDF5_c salt ikm info.

	(* Signature Primitives *)
Fixpoint SIGN(key message: constant) : constant := SIGN_c key message.

Fixpoint SIGNVERIF(gkey message signature: constant) : constant :=
	match gkey, signature with
	| equation_c base exp, SIGN_c key m => match andb (equal_consts exp key) (equal_consts message m) with
											| true => message
											| false => INVALID "SIGNVERIF_fail"
											end
	| _, _ => signature
	end.

Fixpoint RINGSIGN(key_a gkey_b gkey_c message: constant) : constant := RINGSIGN_c key_a gkey_b gkey_c message.

Fixpoint RINGSIGNVERIF(ga gb gc m signature: constant): constant :=
	match signature with
	| RINGSIGN_c key_a b c message => match ga, gb, gc with
									| equation_c base_a exp_a, equation_c base_b exp_b, equation_c base_c exp_c => match orb (orb (equal_consts exp_a key_a) (equal_consts exp_b key_a)) (equal_consts exp_b key_a) with
																												| true => m
																												| false => INVALID "RINGSIGNVERIF_fail_unable_to_auth"
																												end
									| _, _, _ =>  INVALID "RINGSIGNVERIF_fail_key_type_mismatch"
									end
	| _ => signature
	end.

(* Secret Sharing Primitives *)
Fixpoint SHAMIR_SPLIT1 (k: constant) : constant := SHAMIR_SPLIT1_c k.
Fixpoint SHAMIR_SPLIT2 (k: constant) : constant := SHAMIR_SPLIT2_c k.
Fixpoint SHAMIR_SPLIT3 (k: constant) : constant := SHAMIR_SPLIT3_c k.

Fixpoint SHAMIR_JOIN (sa sb: constant) : constant :=
	match sa,sb with
	| SHAMIR_SPLIT1_c ka, SHAMIR_SPLIT2_c kb => match equal_consts ka kb with
												| true => ka
												| false => SHAMIR_JOIN_c sa sb
												end
	| SHAMIR_SPLIT1_c ka, SHAMIR_SPLIT3_c kb => match equal_consts ka kb with
												| true => ka
												| false => SHAMIR_JOIN_c sa sb
												end
	| SHAMIR_SPLIT2_c ka, SHAMIR_SPLIT1_c kb => match equal_consts ka kb with
												| true => ka
												| false => SHAMIR_JOIN_c sa sb
												end
	| SHAMIR_SPLIT2_c ka, SHAMIR_SPLIT3_c kb => match equal_consts ka kb with
												| true => ka
												| false => SHAMIR_JOIN_c sa sb
												end
	| SHAMIR_SPLIT3_c ka, SHAMIR_SPLIT1_c kb => match equal_consts ka kb with
												| true => ka
												| false => SHAMIR_JOIN_c sa sb
												end
	| SHAMIR_SPLIT3_c ka, SHAMIR_SPLIT2_c kb => match equal_consts ka kb with
												| true => ka
												| false => SHAMIR_JOIN_c sa sb
												end
	| _, _ => SHAMIR_JOIN_c sa sb
	end.
	(* Core Primitives *)
Fixpoint ASSERT (c1 c2: constant) : constant  :=
	match equal_consts c1 c2 with
	| true => VALID
	| false => INVALID "ASSERT_fail"
	end.

Fixpoint CONCAT2 (c1 c2: constant) : constant := CONCAT2_c c1 c2.
Fixpoint CONCAT3 (c1 c2 c3: constant) : constant := CONCAT3_c c1 c2 c3.
Fixpoint CONCAT4 (c1 c2 c3 c4: constant) : constant := CONCAT4_c c1 c2 c3 c4.
Fixpoint CONCAT5 (c1 c2 c3 c4 c5: constant) : constant := CONCAT5_c c1 c2 c3 c4 c5.

Fixpoint SPLIT1 (c: constant) : constant :=
	match c with
	| CONCAT2_c c' _ => c'
	| CONCAT3_c c' _ _ => c'
	| CONCAT4_c c' _ _ _ => c'
	| CONCAT5_c c' _ _ _ _ => c'
	| _ => INVALID("Attempting to use SPLIT1 with an incompatible argument")
	end.

Fixpoint SPLIT2 (c: constant) : constant :=
	match c with
	| CONCAT2_c _ c' => c'
	| CONCAT3_c _ c' _ => c'
	| CONCAT4_c _ c' _ _ => c'
	| CONCAT5_c _ c' _ _ _ => c'
	| _ => INVALID("Attempting to use SPLIT2 with an incompatible argument")
	end.

Fixpoint SPLIT3 (c: constant) : constant :=
	match c with
	| CONCAT3_c _ _ c' => c'
	| CONCAT4_c _ _ c' _ => c'
	| CONCAT5_c _ _ c' _ _ => c'
	| _ => INVALID("Attempting to use SPLIT3 with an incompatible argument")
	end.

Fixpoint SPLIT4 (c: constant) : constant :=
	match c with
	| CONCAT4_c _ _ _ c' => c'
	| CONCAT5_c _ _ _ c' _ => c'
	| _ => INVALID("Attempting to use SPLIT4 with an incompatible argument")
	end.

Fixpoint SPLIT5 (c: constant) : constant :=
	match c with
	| CONCAT5_c _ _ _ _ c' => c'
	| _ => INVALID("Attempting to use SPLIT5 with an incompatible argument")
	end.

(*end of primitives*)
Inductive qualifier : Type :=
	| public
	| private
	| password.

Inductive declaration : Type :=
	| assignment
	| knows
	| generates.

Inductive guard_state : Type :=
	| guarded
	| unguarded.

Inductive leak_state : Type :=
	| leaked
	| not_leaked.

Inductive constant_meta: Type :=
	| constant_meta_c (c: constant) (d: declaration) (q: qualifier) (created_by name: string) (l: leak_state)
	| constant_meta_invalid (code: string).

Fixpoint constant_meta_constructor (c: constant) (d: declaration) (q: qualifier) (created_by name: string) :=
	match eqb created_by "", eqb name "" with
	| true, true => constant_meta_invalid "constant_meta must have an non empty value for created_by and name."
	| true, false => constant_meta_invalid "constant_meta must have an non empty value for created_by."
	| false, true => constant_meta_invalid "constant_meta must have an non empty value for name."
	| false, false => constant_meta_c c d q created_by name not_leaked
	end.

Fixpoint get_name_constant_meta (c: constant_meta) : string :=
	match c with
	| constant_meta_invalid code => code
	| constant_meta_c _ _ _ _ name _ => name
	end.

Fixpoint equal_constant_meta (a b: constant_meta) : bool :=
	match a,b with
	| constant_meta_c c1 _ _ _ _ _, constant_meta_c c2 _ _ _ _ _ => equal_consts c1 c2
	| _, _ => false
	end.

Fixpoint leak_constant_meta (cm: constant_meta) : constant_meta :=
	match cm with
	| constant_meta_invalid code => constant_meta_invalid ("Attempting to leak invalid constant_meta; " ++ code)
	| constant_meta_c c d q created_by name _ => constant_meta_c c d q created_by name leaked
	end.

Inductive principal_knowledge: Type :=
	| principal_knowledge_empty
	| principal_knowledge_invalid (code: string)
	| principal_knowledge_c (c: constant_meta) (next: principal_knowledge).

Fixpoint principal_knowledge_constructor (cm: constant_meta) (next: principal_knowledge) : principal_knowledge :=
	match cm with
	| constant_meta_invalid code => principal_knowledge_invalid "Attempting to construct principal_knowledge using invalid constant_meta"
	| constant_meta_c _ _ _ _ _ _ => match next with
									| principal_knowledge_invalid code => principal_knowledge_invalid "Attempting to construct principal_knowledge using invalid provided next principal_knowledge"
									| _ => principal_knowledge_c cm next
									end
		end.

Fixpoint push_pk (pk: principal_knowledge) (cm: constant_meta) : principal_knowledge :=
	match pk with
	| principal_knowledge_invalid code => principal_knowledge_invalid ("Attempting to push constant_meta to invalid principal_knowledge; " ++ code)
	| _ => principal_knowledge_constructor cm pk
	end.

Fixpoint get_constant_meta_by_name_pk (pk: principal_knowledge) (name: string) : constant_meta :=
	match pk with
	| principal_knowledge_invalid code => constant_meta_invalid ("Attempting to get constant_meta from invalid principal_knowledge; " ++ code)
	| principal_knowledge_empty => constant_meta_invalid "Value not found"
	| principal_knowledge_c c next => match eqb name "" with
									| true => constant_meta_invalid "Attempting to get a constant_meta with an empty string as its name"
									| false => match eqb (get_name_constant_meta c) name with
											| true => c
											| false => get_constant_meta_by_name_pk next name
											end
									end
	end.

Fixpoint remove_constant_meta_pk (pk: principal_knowledge) (name: string) : principal_knowledge :=
	match pk with
	| principal_knowledge_empty => pk
	| principal_knowledge_invalid code => principal_knowledge_invalid ("Attempting to remove constant_meta from invalid principal_knowledge; " ++ code)
	| principal_knowledge_c cm next => match eqb name "" with
									| true => principal_knowledge_invalid "Attempting to remove a constant_meta with an empty string as its name"
									| false => match eqb name (get_name_constant_meta cm) with
											| true => next
											| false => principal_knowledge_constructor cm (remove_constant_meta_pk next name)
											end
									end
	end.

Fixpoint update_constant_meta_pk (pk: principal_knowledge) (cm: constant_meta): principal_knowledge :=
	match pk with
	| principal_knowledge_invalid code => principal_knowledge_invalid ("Attempting to update a constant_meta in an invalid principal_knowledge; " ++ code)
	| principal_knowledge_empty => principal_knowledge_invalid "constant_meta not found"
	| principal_knowledge_c _ _ => match cm with
								| constant_meta_invalid _ => principal_knowledge_invalid "Attempting to update a constant_meta using an invalid principal"
								| constant_meta_c _ _ _ _ _ _ => principal_knowledge_constructor cm (remove_constant_meta_pk pk (get_name_constant_meta cm))
								end
	end.

Fixpoint leak_constant_meta_pk (pk: principal_knowledge) (name: string) : principal_knowledge :=
	match pk with
	| principal_knowledge_invalid code => principal_knowledge_invalid ("Attempting to leak constant_meta in invalid principal_knowledge; " ++ code)
	| principal_knowledge_empty => principal_knowledge_invalid "Attempting to leak constant_meta in empty principal_knowledge"
	| principal_knowledge_c _ _ => update_constant_meta_pk pk (leak_constant_meta(get_constant_meta_by_name_pk pk name))
	end.

Inductive principal : Type :=
	| principal_invalid (code: string)
	| principal_c (name: string) (pk: principal_knowledge).

Fixpoint principal_constructor (name: string) (pk: principal_knowledge) : principal :=
	match eqb name "" with
	| true => principal_invalid "Attempt to construct a principal without a name."
	| false => principal_c name pk
	end.

Fixpoint teach_principal (p: principal) (cm: constant_meta) : principal :=
	match p with
	| principal_invalid _ => p
	| principal_c name knowledge => principal_constructor name (push_pk knowledge cm)
	end.

Fixpoint generate_value (p: principal) (s: string) : principal :=
	match eqb "" s with
	| true => principal_invalid "Generated value must have a non empty string as its name."
	| false => match p with
			| principal_invalid _ => p
			| principal_c name _ => teach_principal p (constant_meta_constructor (value s) generates private name s)
			end
	end.

Fixpoint know_value (p: principal) (s: string) (q: qualifier) : principal :=
	match eqb "" s with
	| true => principal_invalid "Value to be known must have a non empty string as its name."
	| false => match p with
			| principal_invalid _ => p
			| principal_c name _ => teach_principal p (constant_meta_constructor (value s) knows q name s)
			end
	end.

Fixpoint assign_value (p: principal) (c: constant) (s: string) : principal :=
	match eqb "" s with
	| true => principal_invalid "Assigned value must have a non empty string as its name."
	| false => match p with
			| principal_invalid code => p
			| principal_c name _ => teach_principal p (constant_meta_constructor c assignment private name s)
			end
	end.

Fixpoint get_name_principal (p: principal) : string :=
	match p with
	| principal_invalid code => code
	| principal_c name _ => name
	end.

Fixpoint get_constant_meta_by_name_principal (p: principal) (name: string) : constant_meta :=
	match eqb "" name with
	| true => constant_meta_invalid "Attempting to look for a value with an empty string as its name"
	| false => match p with
			| principal_invalid _ => constant_meta_invalid "Value not found."
			| principal_c _ k => get_constant_meta_by_name_pk k name
			end
	end.

Fixpoint leak_value (p: principal) (value_name: string) : principal :=
	match eqb "" value_name with
	| true => principal_invalid "Attepmting to leak a value with an invalid name."
	| false => match p with
				| principal_invalid code => principal_invalid ("Attempting to leak a value in an invalid principal; " ++ code)
				| principal_c principal_name pk => principal_constructor principal_name (leak_constant_meta_pk pk value_name)
				end
	end.

Fixpoint get (p: principal) (name: string) : constant :=
	match (get_constant_meta_by_name_principal p name) with
	| constant_meta_invalid code => INVALID code
	| constant_meta_c c' _ _ _ _ _ => c'
	end.

Inductive principal_list : Type :=
	| principal_list_invalid (code: string)
	| principal_list_empty
	| principal_list_c (p: principal) (next: principal_list).

Fixpoint principal_list_constructor (p: principal) (next: principal_list) : principal_list :=
	match p with
	| principal_invalid code => principal_list_invalid ("Cannot construct principal_list using invalid principal; " ++ code)
	| principal_c _ _ => match next with
						| principal_list_invalid code => principal_list_invalid ("Cannot construct principal_list using invalid next principal_list; " ++ code)
						| _ => principal_list_c p next
						end
		end.

Fixpoint add_principal (list: principal_list) (p: principal) : principal_list :=
	match list with
	| principal_list_invalid code => principal_list_invalid ("Cannot add principal to invalid list; " ++ code)
	| principal_list_empty => principal_list_constructor p list
	| principal_list_c _ next => principal_list_constructor p list
	end.

Fixpoint remove_principal (list: principal_list) (name: string) : principal_list :=
	match list with
	| principal_list_invalid code => principal_list_invalid ("Attempting to remove a principal from an invalid principal_list; " ++ code)
	| principal_list_empty => principal_list_invalid "Principal not found"
	| principal_list_c p next => match eqb name "" with
								| true => principal_list_invalid "Attempting to remove a principal with an empty string as its name"
								| false => match eqb name (get_name_principal p) with
										| true => next
										| false => principal_list_constructor p (remove_principal next name)
										end
								end
	end.
Fixpoint update_principal (list: principal_list) (p: principal): principal_list :=
		match list with
		| principal_list_invalid code => principal_list_invalid ("Attempting to update a principal in an invalid principal_list; " ++ code)
		| principal_list_empty => principal_list_invalid "Principal not found"
		| principal_list_c _ _ => match p with
								| principal_invalid _ => principal_list_invalid "Attempting to update a principal_list using an invalid principal"
								| principal_c _ _ => principal_list_constructor p (remove_principal list (get_name_principal p))
								end
		end.

Fixpoint get_principal_by_name_principal_list (list: principal_list) (name: string) : principal :=
		match list with
		| principal_list_invalid code => principal_invalid ("Attempting to get a principal from an invalid principal_list; " ++ code)
		| principal_list_empty => principal_invalid "Principal not found"
		| principal_list_c p list' => match eqb name "" with
									| true => principal_invalid "The provided name for the principal cannot be empty"
									| false => match eqb (get_name_principal p) name with
											| true => p
											| false => get_principal_by_name_principal_list list' name
											end
									end
		end.

Fixpoint teach_principal_principal_list (list: principal_list) (principal_name: string) (cm: constant_meta) : principal_list :=
	match cm with
	| constant_meta_invalid code => principal_list_invalid ("Attempting to teach an invalid constant_meta to a principal; " ++ code)
	| constant_meta_c _ _ _ _ _ _ => match eqb principal_name "" with
									| true => principal_list_invalid "The provided name for the principal cannot be empty"
									| false => match list with
											| principal_list_invalid code => principal_list_invalid ("Attempting to teach a principal in an invalid principal_list; " ++ code)
											| principal_list_empty => add_principal list (teach_principal (principal_constructor principal_name principal_knowledge_empty) cm)
											| principal_list_c p list' => update_principal list (teach_principal (get_principal_by_name_principal_list list principal_name) cm)
											end
									end
	end.

Inductive message : Type :=
		| message_c (from to value_name: string) (g: guard_state)
		| message_invalid (code: string).

Fixpoint message_constructor (from to value_name: string) (g: guard_state) :=
	match eqb "" from, eqb "" to, eqb "" value_name with
	| true, _, _ => message_invalid "The value of from cannot be empty"
	| _, true, _ => message_invalid "The value of to cannot be empty"
	| _, _, true => message_invalid "The value of value_name cannot be empty"
	| false, false, false => message_c from to value_name g
	end.

Inductive message_list : Type :=
	| message_list_invalid (code: string)
	| message_list_empty
	| message_list_c (m: message) (next: message_list).

Fixpoint message_list_constructor (m: message) : message_list :=
	match m with
	| message_invalid _ => message_list_invalid "Attempting to construct message_list using an invalid message"
	| message_c _ _ _ _ => message_list_c m message_list_empty
	end.

Fixpoint add_message_to_list (list: message_list) (m: message) : message_list :=
	match m with
	| message_invalid _ => message_list_invalid "Attempting to add invalid message to list"
	| message_c _ _ _ _ => match list with
						| message_list_invalid _ => message_list_invalid "Attempting to add message to invalid message_list"
						| message_list_empty => message_list_constructor m
						| message_list_c _ next => add_message_to_list next m
						end
	end.

Inductive knowledgemap : Type :=
		| knowledgemap_invalid (code: string)
		| knowledgemap_c (list: principal_list) (messages: message_list).

Fixpoint knowledgemap_constructor (principal_name: string) : knowledgemap :=
	match eqb principal_name "" with
	| true => knowledgemap_invalid "Attempting to construct knowledge map with empty principal name"
	| false => knowledgemap_c (principal_list_constructor (principal_constructor principal_name principal_knowledge_empty) principal_list_empty) message_list_empty
	end.

Fixpoint add_principal_knowledgemap (k: knowledgemap) (name: string) : knowledgemap :=
	match k with
	| knowledgemap_invalid code => knowledgemap_invalid ("Attempting to add principal to invalid knowledgemap; " ++ code)
	| knowledgemap_c list m => knowledgemap_c (add_principal list (principal_constructor name principal_knowledge_empty)) m
	end.

Fixpoint get_principal_knowledgemap (k: knowledgemap) (name: string) : principal :=
	match k with
	| knowledgemap_invalid code => principal_invalid ("Attempting to get principal from invalid knowledgemap; " ++ code)
	| knowledgemap_c list _ => get_principal_by_name_principal_list list name
	end.

Fixpoint update_principal_knowledgemap (k: knowledgemap) (p: principal) : knowledgemap :=
	match k with
	| knowledgemap_invalid code => knowledgemap_invalid ("Attempting to update principal in invalid knowledgemap; " ++ code)
	| knowledgemap_c list m => knowledgemap_c (update_principal list p) m
	end.

Fixpoint add_message_knowledgemap (k: knowledgemap) (m: message) : knowledgemap :=
	match k with
	| knowledgemap_invalid code => knowledgemap_invalid ("Attempting to add message to invalid knowledgemap; " ++ code)
	| knowledgemap_c list messages => knowledgemap_c list (add_message_to_list messages m)
	end.

Fixpoint send_message (s: knowledgemap): knowledgemap :=
	match s with
	| knowledgemap_invalid _ => knowledgemap_invalid "Attempting to send a message using an invalid knowledgemap"
	| knowledgemap_c list messages => match messages with
									| message_list_invalid _ => knowledgemap_invalid "Invalid message list"
									| message_list_empty => s
									| message_list_c m next => match m with
															| message_invalid _ => knowledgemap_invalid "Attempting to send an invalid message"
															| message_c from to value_name g => match get_principal_by_name_principal_list list from with
																							| principal_invalid code => knowledgemap_invalid ("The sender provided is not valid; " ++ code)
																							| principal_c _ sender_pk => match get_constant_meta_by_name_pk sender_pk value_name with
																														| constant_meta_invalid code => knowledgemap_invalid ("The sender does now list know the value being sent; " ++ code)
																														| constant_meta_c _ _ _ _ _ _ => match get_principal_by_name_principal_list list to with
																																						| principal_invalid code => knowledgemap_invalid ("The recipient provided is not valid; " ++ code)
																																						| principal_c _ recipient_pk => knowledgemap_c (teach_principal_principal_list list to (get_constant_meta_by_name_pk sender_pk value_name)) next
																																						end
																														end
																							end
															end
									end
	end.


(* Protocol: signal.vp *)

Definition kmap_0 := knowledgemap_constructor "Alice".
Definition kmap_1 := add_principal_knowledgemap kmap_0 "Alice".
Definition kmap_2 := add_principal_knowledgemap kmap_1 "Bob".
Definition principal_alice_0 := get_principal_knowledgemap kmap_2 "Alice".
Definition principal_alice_1 := know_value principal_alice_0 "c0" public.
Definition principal_alice_2 := know_value principal_alice_1 "c1" public.
Definition principal_alice_3 := know_value principal_alice_2 "c2" public.
Definition principal_alice_4 := know_value principal_alice_3 "c3" public.
Definition principal_alice_5 := know_value principal_alice_4 "c4" public.
Definition principal_alice_6 := know_value principal_alice_5 "alongterm" private.
Definition principal_alice_7 := assign_value principal_alice_6 (public_key (get principal_alice_6 "alongterm")) "galongterm".
Definition kmap_3 := update_principal_knowledgemap kmap_2 principal_alice_7.
Definition principal_bob_0 := get_principal_knowledgemap kmap_3 "Bob".
Definition principal_bob_1 := know_value principal_bob_0 "c0" public.
Definition principal_bob_2 := know_value principal_bob_1 "c1" public.
Definition principal_bob_3 := know_value principal_bob_2 "c2" public.
Definition principal_bob_4 := know_value principal_bob_3 "c3" public.
Definition principal_bob_5 := know_value principal_bob_4 "c4" public.
Definition principal_bob_6 := know_value principal_bob_5 "blongterm" private.
Definition principal_bob_7 := know_value principal_bob_6 "bs" private.
Definition principal_bob_8 := generate_value principal_bob_7 "bo".
Definition principal_bob_9 := assign_value principal_bob_8 (public_key (get principal_bob_8 "blongterm")) "gblongterm".
Definition principal_bob_10 := assign_value principal_bob_9 (public_key (get principal_bob_9 "bs")) "gbs".
Definition principal_bob_11 := assign_value principal_bob_10 (public_key (get principal_bob_10 "bo")) "gbo".
Definition principal_bob_12 := assign_value principal_bob_11 (SIGN (get principal_bob_11 "blongterm") (get principal_bob_11 "gbs")) "gbssig".
Definition kmap_4 := update_principal_knowledgemap kmap_3 principal_bob_12.
Definition kmap_5 := add_message_knowledgemap kmap_4 (message_constructor "Bob" "Alice" "gblongterm" guarded).
Definition kmap_6 := send_message kmap_5.
Definition kmap_7 := add_message_knowledgemap kmap_6 (message_constructor "Bob" "Alice" "gbssig" unguarded).
Definition kmap_8 := send_message kmap_7.
Definition kmap_9 := add_message_knowledgemap kmap_8 (message_constructor "Bob" "Alice" "gbs" unguarded).
Definition kmap_10 := send_message kmap_9.
Definition kmap_11 := add_message_knowledgemap kmap_10 (message_constructor "Bob" "Alice" "gbo" unguarded).
Definition kmap_12 := send_message kmap_11.
Definition principal_alice_8 := get_principal_knowledgemap kmap_12 "Alice".
Definition principal_alice_9 := generate_value principal_alice_8 "ae1".
Definition principal_alice_10 := assign_value principal_alice_9 (public_key (get principal_alice_9 "ae1")) "gae1".
Definition principal_alice_11 := assign_value principal_alice_10 (DH (get principal_alice_10 "gbs")(get principal_alice_10 "alongterm")) "unnamed_0".
Definition principal_alice_12 := assign_value principal_alice_11 (DH (get principal_alice_11 "gblongterm")(get principal_alice_11 "ae1")) "unnamed_1".
Definition principal_alice_13 := assign_value principal_alice_12 (DH (get principal_alice_12 "gbs")(get principal_alice_12 "ae1")) "unnamed_2".
Definition principal_alice_14 := assign_value principal_alice_13 (DH (get principal_alice_13 "gbo")(get principal_alice_13 "ae1")) "unnamed_3".
Definition principal_alice_15 := assign_value principal_alice_14 (HASH5 (get principal_alice_10 "c0") (get principal_alice_11 "unnamed_0") (get principal_alice_12 "unnamed_1") (get principal_alice_13 "unnamed_2") (get principal_alice_14 "unnamed_3")) "amaster".
Definition principal_alice_16 := assign_value principal_alice_15 (HKDF1 (get principal_alice_15 "amaster") (get principal_alice_15 "c1") (get principal_alice_15 "c2")) "arkba1".
Definition principal_alice_17 := assign_value principal_alice_16 (HKDF2 (get principal_alice_16 "amaster") (get principal_alice_16 "c1") (get principal_alice_16 "c2")) "ackba1".
Definition kmap_13 := update_principal_knowledgemap kmap_12 principal_alice_17.
Definition principal_alice_18 := get_principal_knowledgemap kmap_13 "Alice".
Definition principal_alice_19 := generate_value principal_alice_18 "m1".
Definition principal_alice_20 := generate_value principal_alice_19 "ae2".
Definition principal_alice_21 := assign_value principal_alice_20 (public_key (get principal_alice_20 "ae2")) "gae2".
Definition principal_alice_22 := assign_value principal_alice_21 (SIGNVERIF (get principal_alice_21 "gblongterm") (get principal_alice_21 "gbs") (get principal_alice_21 "gbssig")) "unnamed_0".
Definition principal_alice_23 := assign_value principal_alice_22 (DH (get principal_alice_22 "gbs")(get principal_alice_22 "ae2")) "akshared1".
Definition principal_alice_24 := assign_value principal_alice_23 (HKDF1 (get principal_alice_23 "akshared1") (get principal_alice_23 "arkba1") (get principal_alice_23 "c2")) "arkab1".
Definition principal_alice_25 := assign_value principal_alice_24 (HKDF2 (get principal_alice_24 "akshared1") (get principal_alice_24 "arkba1") (get principal_alice_24 "c2")) "ackab1".
Definition principal_alice_26 := assign_value principal_alice_25 (MAC (get principal_alice_25 "ackab1") (get principal_alice_25 "c3")) "unnamed_4".
Definition principal_alice_27 := assign_value principal_alice_26 (HKDF1 (get principal_alice_26 "unnamed_4") (get principal_alice_26 "c1") (get principal_alice_26 "c4")) "akenc1".
Definition principal_alice_28 := assign_value principal_alice_27 (MAC (get principal_alice_27 "ackab1") (get principal_alice_27 "c3")) "unnamed_5".
Definition principal_alice_29 := assign_value principal_alice_28 (HKDF2 (get principal_alice_28 "unnamed_5") (get principal_alice_28 "c1") (get principal_alice_28 "c4")) "akenc2".
Definition principal_alice_30 := assign_value principal_alice_29 (HASH3 (get principal_alice_29 "galongterm") (get principal_alice_29 "gblongterm") (get principal_alice_29 "gae2")) "unnamed_6".
Definition principal_alice_31 := assign_value principal_alice_30 (AEAD_ENC (get principal_alice_29 "akenc1") (get principal_alice_29 "m1") (get principal_alice_30 "unnamed_6")) "e1".
Definition kmap_14 := update_principal_knowledgemap kmap_13 principal_alice_31.
Definition kmap_15 := add_message_knowledgemap kmap_14 (message_constructor "Alice" "Bob" "galongterm" guarded).
Definition kmap_16 := send_message kmap_15.
Definition kmap_17 := add_message_knowledgemap kmap_16 (message_constructor "Alice" "Bob" "gae1" unguarded).
Definition kmap_18 := send_message kmap_17.
Definition kmap_19 := add_message_knowledgemap kmap_18 (message_constructor "Alice" "Bob" "gae2" unguarded).
Definition kmap_20 := send_message kmap_19.
Definition kmap_21 := add_message_knowledgemap kmap_20 (message_constructor "Alice" "Bob" "e1" unguarded).
Definition kmap_22 := send_message kmap_21.
Definition principal_bob_13 := get_principal_knowledgemap kmap_22 "Bob".
Definition principal_bob_14 := assign_value principal_bob_13 (DH (get principal_bob_13 "galongterm")(get principal_bob_13 "bs")) "unnamed_7".
Definition principal_bob_15 := assign_value principal_bob_14 (DH (get principal_bob_14 "gae1")(get principal_bob_14 "blongterm")) "unnamed_8".
Definition principal_bob_16 := assign_value principal_bob_15 (DH (get principal_bob_15 "gae1")(get principal_bob_15 "bs")) "unnamed_9".
Definition principal_bob_17 := assign_value principal_bob_16 (DH (get principal_bob_16 "gae1")(get principal_bob_16 "bo")) "unnamed_10".
Definition principal_bob_18 := assign_value principal_bob_17 (HASH5 (get principal_bob_13 "c0") (get principal_bob_14 "unnamed_7") (get principal_bob_15 "unnamed_8") (get principal_bob_16 "unnamed_9") (get principal_bob_17 "unnamed_10")) "bmaster".
Definition principal_bob_19 := assign_value principal_bob_18 (HKDF1 (get principal_bob_18 "bmaster") (get principal_bob_18 "c1") (get principal_bob_18 "c2")) "brkba1".
Definition principal_bob_20 := assign_value principal_bob_19 (HKDF2 (get principal_bob_19 "bmaster") (get principal_bob_19 "c1") (get principal_bob_19 "c2")) "bckba1".
Definition kmap_23 := update_principal_knowledgemap kmap_22 principal_bob_20.
Definition principal_bob_21 := get_principal_knowledgemap kmap_23 "Bob".
Definition principal_bob_22 := assign_value principal_bob_21 (DH (get principal_bob_21 "gae2")(get principal_bob_21 "bs")) "bkshared1".
Definition principal_bob_23 := assign_value principal_bob_22 (HKDF1 (get principal_bob_22 "bkshared1") (get principal_bob_22 "brkba1") (get principal_bob_22 "c2")) "brkab1".
Definition principal_bob_24 := assign_value principal_bob_23 (HKDF2 (get principal_bob_23 "bkshared1") (get principal_bob_23 "brkba1") (get principal_bob_23 "c2")) "bckab1".
Definition principal_bob_25 := assign_value principal_bob_24 (MAC (get principal_bob_24 "bckab1") (get principal_bob_24 "c3")) "unnamed_11".
Definition principal_bob_26 := assign_value principal_bob_25 (HKDF1 (get principal_bob_25 "unnamed_11") (get principal_bob_25 "c1") (get principal_bob_25 "c4")) "bkenc1".
Definition principal_bob_27 := assign_value principal_bob_26 (MAC (get principal_bob_26 "bckab1") (get principal_bob_26 "c3")) "unnamed_12".
Definition principal_bob_28 := assign_value principal_bob_27 (HKDF2 (get principal_bob_27 "unnamed_12") (get principal_bob_27 "c1") (get principal_bob_27 "c4")) "bkenc2".
Definition principal_bob_29 := assign_value principal_bob_28 (HASH3 (get principal_bob_28 "galongterm") (get principal_bob_28 "gblongterm") (get principal_bob_28 "gae2")) "unnamed_13".
Definition principal_bob_30 := assign_value principal_bob_29 (AEAD_DEC (get principal_bob_28 "bkenc1") (get principal_bob_28 "e1") (get principal_bob_29 "unnamed_13")) "m1_d".
Definition kmap_24 := update_principal_knowledgemap kmap_23 principal_bob_30.
Definition principal_bob_31 := get_principal_knowledgemap kmap_24 "Bob".
Definition principal_bob_32 := generate_value principal_bob_31 "m2".
Definition principal_bob_33 := generate_value principal_bob_32 "be".
Definition principal_bob_34 := assign_value principal_bob_33 (public_key (get principal_bob_33 "be")) "gbe".
Definition principal_bob_35 := assign_value principal_bob_34 (DH (get principal_bob_34 "gae2")(get principal_bob_34 "be")) "bkshared2".
Definition principal_bob_36 := assign_value principal_bob_35 (HKDF1 (get principal_bob_35 "bkshared2") (get principal_bob_35 "brkab1") (get principal_bob_35 "c2")) "brkba2".
Definition principal_bob_37 := assign_value principal_bob_36 (HKDF2 (get principal_bob_36 "bkshared2") (get principal_bob_36 "brkab1") (get principal_bob_36 "c2")) "bckba2".
Definition principal_bob_38 := assign_value principal_bob_37 (MAC (get principal_bob_37 "bckba2") (get principal_bob_37 "c3")) "unnamed_14".
Definition principal_bob_39 := assign_value principal_bob_38 (HKDF1 (get principal_bob_38 "unnamed_14") (get principal_bob_38 "c1") (get principal_bob_38 "c4")) "bkenc3".
Definition principal_bob_40 := assign_value principal_bob_39 (MAC (get principal_bob_39 "bckba2") (get principal_bob_39 "c3")) "unnamed_15".
Definition principal_bob_41 := assign_value principal_bob_40 (HKDF2 (get principal_bob_40 "unnamed_15") (get principal_bob_40 "c1") (get principal_bob_40 "c4")) "bkenc4".
Definition principal_bob_42 := assign_value principal_bob_41 (HASH3 (get principal_bob_41 "gblongterm") (get principal_bob_41 "galongterm") (get principal_bob_41 "gbe")) "unnamed_16".
Definition principal_bob_43 := assign_value principal_bob_42 (AEAD_ENC (get principal_bob_41 "bkenc3") (get principal_bob_41 "m2") (get principal_bob_42 "unnamed_16")) "e2".
Definition kmap_25 := update_principal_knowledgemap kmap_24 principal_bob_43.
Definition kmap_26 := add_message_knowledgemap kmap_25 (message_constructor "Bob" "Alice" "gbe" unguarded).
Definition kmap_27 := send_message kmap_26.
Definition kmap_28 := add_message_knowledgemap kmap_27 (message_constructor "Bob" "Alice" "e2" unguarded).
Definition kmap_29 := send_message kmap_28.
Definition principal_alice_32 := get_principal_knowledgemap kmap_29 "Alice".
Definition principal_alice_33 := assign_value principal_alice_32 (DH (get principal_alice_32 "gbe")(get principal_alice_32 "ae2")) "akshared2".
Definition principal_alice_34 := assign_value principal_alice_33 (HKDF1 (get principal_alice_33 "akshared2") (get principal_alice_33 "arkab1") (get principal_alice_33 "c2")) "arkba2".
Definition principal_alice_35 := assign_value principal_alice_34 (HKDF2 (get principal_alice_34 "akshared2") (get principal_alice_34 "arkab1") (get principal_alice_34 "c2")) "ackba2".
Definition principal_alice_36 := assign_value principal_alice_35 (MAC (get principal_alice_35 "ackba2") (get principal_alice_35 "c3")) "unnamed_17".
Definition principal_alice_37 := assign_value principal_alice_36 (HKDF1 (get principal_alice_36 "unnamed_17") (get principal_alice_36 "c1") (get principal_alice_36 "c4")) "akenc3".
Definition principal_alice_38 := assign_value principal_alice_37 (MAC (get principal_alice_37 "ackba2") (get principal_alice_37 "c3")) "unnamed_18".
Definition principal_alice_39 := assign_value principal_alice_38 (HKDF2 (get principal_alice_38 "unnamed_18") (get principal_alice_38 "c1") (get principal_alice_38 "c4")) "akenc4".
Definition principal_alice_40 := assign_value principal_alice_39 (HASH3 (get principal_alice_39 "gblongterm") (get principal_alice_39 "galongterm") (get principal_alice_39 "gbe")) "unnamed_19".
Definition principal_alice_41 := assign_value principal_alice_40 (AEAD_DEC (get principal_alice_39 "akenc3") (get principal_alice_39 "e2") (get principal_alice_40 "unnamed_19")) "m2_d".
Definition kmap_30 := update_principal_knowledgemap kmap_29 principal_alice_41.
Definition principal_alice_42 := get_principal_knowledgemap kmap_30 "Alice".
Definition principal_alice_43 := generate_value principal_alice_42 "m3".
Definition principal_alice_44 := generate_value principal_alice_43 "ae3".
Definition principal_alice_45 := assign_value principal_alice_44 (public_key (get principal_alice_44 "ae3")) "gae3".
Definition principal_alice_46 := assign_value principal_alice_45 (DH (get principal_alice_45 "gbe")(get principal_alice_45 "ae3")) "akshared3".
Definition principal_alice_47 := assign_value principal_alice_46 (HKDF1 (get principal_alice_46 "akshared3") (get principal_alice_46 "arkba2") (get principal_alice_46 "c2")) "arkab3".
Definition principal_alice_48 := assign_value principal_alice_47 (HKDF2 (get principal_alice_47 "akshared3") (get principal_alice_47 "arkba2") (get principal_alice_47 "c2")) "ackab3".
Definition principal_alice_49 := assign_value principal_alice_48 (MAC (get principal_alice_48 "ackab3") (get principal_alice_48 "c3")) "unnamed_20".
Definition principal_alice_50 := assign_value principal_alice_49 (HKDF1 (get principal_alice_49 "unnamed_20") (get principal_alice_49 "c1") (get principal_alice_49 "c4")) "akenc5".
Definition principal_alice_51 := assign_value principal_alice_50 (MAC (get principal_alice_50 "ackab3") (get principal_alice_50 "c3")) "unnamed_21".
Definition principal_alice_52 := assign_value principal_alice_51 (HKDF2 (get principal_alice_51 "unnamed_21") (get principal_alice_51 "c1") (get principal_alice_51 "c4")) "akenc6".
Definition principal_alice_53 := assign_value principal_alice_52 (HASH3 (get principal_alice_52 "gblongterm") (get principal_alice_52 "galongterm") (get principal_alice_52 "gae3")) "unnamed_22".
Definition principal_alice_54 := assign_value principal_alice_53 (AEAD_ENC (get principal_alice_52 "akenc5") (get principal_alice_52 "m3") (get principal_alice_53 "unnamed_22")) "e3".
Definition kmap_31 := update_principal_knowledgemap kmap_30 principal_alice_54.
Definition kmap_32 := add_message_knowledgemap kmap_31 (message_constructor "Alice" "Bob" "gae3" unguarded).
Definition kmap_33 := send_message kmap_32.
Definition kmap_34 := add_message_knowledgemap kmap_33 (message_constructor "Alice" "Bob" "e3" unguarded).
Definition kmap_35 := send_message kmap_34.
Definition principal_bob_44 := get_principal_knowledgemap kmap_35 "Bob".
Definition principal_bob_45 := assign_value principal_bob_44 (DH (get principal_bob_44 "gae3")(get principal_bob_44 "be")) "bkshared3".
Definition principal_bob_46 := assign_value principal_bob_45 (HKDF1 (get principal_bob_45 "bkshared3") (get principal_bob_45 "brkba2") (get principal_bob_45 "c2")) "brkab3".
Definition principal_bob_47 := assign_value principal_bob_46 (HKDF2 (get principal_bob_46 "bkshared3") (get principal_bob_46 "brkba2") (get principal_bob_46 "c2")) "bckab3".
Definition principal_bob_48 := assign_value principal_bob_47 (MAC (get principal_bob_47 "bckab3") (get principal_bob_47 "c3")) "unnamed_23".
Definition principal_bob_49 := assign_value principal_bob_48 (HKDF1 (get principal_bob_48 "unnamed_23") (get principal_bob_48 "c1") (get principal_bob_48 "c4")) "bkenc5".
Definition principal_bob_50 := assign_value principal_bob_49 (MAC (get principal_bob_49 "bckab3") (get principal_bob_49 "c3")) "unnamed_24".
Definition principal_bob_51 := assign_value principal_bob_50 (HKDF2 (get principal_bob_50 "unnamed_24") (get principal_bob_50 "c1") (get principal_bob_50 "c4")) "bkenc6".
Definition principal_bob_52 := assign_value principal_bob_51 (HASH3 (get principal_bob_51 "gblongterm") (get principal_bob_51 "galongterm") (get principal_bob_51 "gae3")) "unnamed_25".
Definition principal_bob_53 := assign_value principal_bob_52 (AEAD_DEC (get principal_bob_51 "bkenc5") (get principal_bob_51 "e3") (get principal_bob_52 "unnamed_25")) "m3_d".
Definition kmap_36 := update_principal_knowledgemap kmap_35 principal_bob_53.
Definition principal_alice_55 := get_principal_knowledgemap kmap_36 "Alice".
Definition principal_alice_56 := leak_value principal_alice_55 "alongterm".
Definition kmap_37 := update_principal_knowledgemap kmap_36 principal_alice_56.
Definition principal_bob_54 := get_principal_knowledgemap kmap_37 "Bob".
Definition principal_bob_55 := leak_value principal_bob_54 "blongterm".
Definition kmap_38 := update_principal_knowledgemap kmap_37 principal_bob_55.
Compute(update_principal_knowledgemap kmap_37 principal_bob_55).