(** Perfect Crypto - Simple definitions for message encryption and signing using symmetric and assymetric keys Perry Alexander The University of Kansas Provides definitions for: - [keyType] - [symmetric], [public] and [private] key constructors. - [inverse] - defines the inverse of any key. - [is_inverse] - proof that [inverse] is decidable and provides a decision procesure for [inverse]. - [is_not_decryptable] - predicate indicating that a message is or is not decryptable using a specified key. - [decrypt] - attempts to decrypt a message with a given key. Returns the decrypted message if decryption occurs. Returns a proof that the message cannot be decrypted with the key if decryption does not occur. - [is_signed] - proof that signature checking is decidable and provides a decision procedure for signature check. - [check] - checks a signature on a message with a given key. Returns a proof that the check succeeds or does not succeed. - [check_dec] - proof that signature checking is decidable and provides a decision procedure for signature checking. Alternative function for [check]. *) Require Import Omega. (** Key values will be [nat] *) Definition key_val : Type := nat. (** Key types are [symmetric], [public] and [private]. *) Inductive keyType: Type := | symmetric : key_val -> keyType | private : key_val -> keyType | public : key_val -> keyType. (** A [symmetric] key is its own inverse. A [public] key is the inverse of the [private] key with the same [key_val]. A [private] key is the inverse of the [public] key with the same [key_val]. *) Fixpoint inverse(k:keyType):keyType := match k with | symmetric k => symmetric k | public k => private k | private k => public k end. (** Proof that inverse is decidable for any two keys. The resulting proof gives us the function [is_inverse] that is a decision procedure for key inverse checking. It will be used in [decrypt] and [check] later in the specification. *) Theorem is_inverse:forall k k', {k = (inverse k')}+{k <> (inverse k')}. Proof. intros k k'; destruct k; destruct k'; try (right; simpl; discriminate); try (destruct (eq_nat_dec k k0) as [Hinv | Hninv]; [ left; simpl; auto | right; simpl; unfold not; intros H; inversion H; contradiction ]). Defined. Eval compute in (is_inverse (public 1) (private 1)). Eval compute in (is_inverse (public 1) (private 2)). Eval compute in (is_inverse (public 2) (private 1)). Eval compute in (is_inverse (private 1) (public 1)). Eval compute in (is_inverse (symmetric 1) (symmetric 1)). Eval compute in (is_inverse (symmetric 1) (symmetric 2)). Compute (is_inverse (symmetric 1) (symmetric 2)). (** Various proofs for keys and properties of the inverse operation. All keys must have an inverse. All keys have a unique inverse. Equal inverses come from equal keys *) Theorem inverse_injective : forall k1 k2, inverse k1 = inverse k2 -> k1 = k2. Proof. intros k1 k2 H. destruct k1; destruct k2; simpl in H; inversion H; reflexivity. Qed. Hint Resolve inverse_injective. Theorem inverse_inverse : forall k, inverse (inverse k) = k. Proof. intros k; destruct k; reflexivity. Qed. Hint Resolve inverse_inverse. (** Check this. May be total, not surjective. *) Theorem inverse_surjective : forall k, exists k', (inverse k) = k'. Proof. intros k. exists (inverse k). reflexivity. Qed. Hint Resolve inverse_surjective. Theorem inverse_bijective : forall k k', inverse k = inverse k' -> k = k' /\ forall k, exists k'', inverse k = k''. Proof. auto. Restart. intros k k' H. split. apply inverse_injective. assumption. apply inverse_surjective. Qed. (** Basic messages held abstract. Compound messages are keys, encrypted and signed messages, hashes and pairs. *) Inductive message(basicType:Type) : Type := | basic : basicType -> message basicType | key : keyType -> message basicType | encrypt : message basicType -> keyType -> message basicType | sign : message basicType -> keyType -> message basicType | hash : message basicType -> message basicType | pair : message basicType -> message basicType -> message basicType. (** Predicate that determines if a message cannot be decrypted. Could be that it is not encrypted to begin with or the wrong key is used. *) Definition is_not_decryptable{T:Type}(m:message T)(k:keyType):Prop := match m with | basic _ _ => True | key _ _ => True | encrypt _ m' k' => k <> inverse k' | sign _ _ _ => True | hash _ _ => True | pair _ _ _ => True end. (** [decrypt] returns either a decrypted message or a proof of why the message cannot be decrypted. *) Fixpoint decrypt{T:Type}(m:message T)(k:keyType):(message T)+{(is_not_decryptable m k)}. refine match m with | basic _ c => inright _ _ | key _ _ => inright _ _ | encrypt _ m' j => (if (is_inverse k j) then (inleft _ m') else (inright _ _ )) | sign _ m' k => inright _ _ | hash _ _ => inright _ _ | pair _ _ _ => inright _ _ end. Proof. reflexivity. reflexivity. simpl. assumption. reflexivity. reflexivity. reflexivity. Defined. Eval compute in decrypt(encrypt nat (basic nat 1) (symmetric 1)) (symmetric 1). Eval compute in decrypt(encrypt nat (basic nat 1) (symmetric 1)) (symmetric 2). (** Predicate that determines if a message is properly signed. *) Definition is_signed{T:Type}(m:message T)(k:keyType):Prop := match m with | basic _ _ => False | key _ _ => False | encrypt _ _ _ => False | sign _ m' k' => k = inverse k' | hash _ _ => False | pair _ _ _ => False end. (** Signature check returns either a proof that the signature is correct or a proof that the signature is not correct. *) Fixpoint check{T:Type}(m:message T)(k:keyType):{(is_signed m k)}+{not (is_signed m k)}. refine match m with | basic _ c => right _ _ | key _ _ => right _ _ | sign _ m' j => (if (is_inverse k j) then (left _ _) else (right _ _ )) | encrypt _ m' k => right _ _ | hash _ _ => right _ _ | pair _ _ _ => right _ _ end. Proof. unfold not. intros. simpl in H. assumption. unfold not. intros. simpl in H. assumption. unfold not. intros. simpl in H. assumption. destruct (is_inverse j k). simpl. assumption. simpl. assumption. simpl. assumption. unfold not. intros. simpl in H. assumption. unfold not. intros. simpl in H. assumption. Defined. Eval compute in check(sign nat (basic nat 1) (private 1)) (public 1). Eval compute in check(sign nat (basic nat 1) (private 1)) (public 2). Theorem check_dec: forall T, forall m:(message T), forall k, {(is_signed m k)}+{not (is_signed m k)}. Proof. intros. destruct m. right. unfold is_signed. tauto. right. unfold is_signed. tauto. right. unfold is_signed. tauto. destruct (is_inverse k0 k). left. simpl. rewrite e. auto. right. unfold not. simpl. unfold not in n. intros. subst. auto. right. unfold is_signed. tauto. right. unfold is_signed. tauto. Defined. Eval compute in check_dec nat (sign nat (basic nat 1) (private 1)) (public 1). Eval compute in check_dec nat (sign nat (basic nat 1) (private 1)) (public 2).