(** * Example of manipulation of inductive definitions *)
(** Needham-Schroeder protocol *)
(** simplified bversion without a server for distributing public keys *)
(** version without flaw *)
(** ** Basic data types *)
(** - Users;
- Agents : A is Alice, B is Bob, I is the intruder
- Keys and data: keys will be asymmetric and public;
- Messages: the keys, or names of agents,
or nonces generated by one agent for another;
messages can be encoded with the public key of an agent and paired.
*)
Inductive agent : Set := A | B | I .
Inductive message : Set :=
Name : agent -> message
| Nonce : agent * agent -> message
| SK : agent -> message
| Enc : message -> agent -> message
| P : message -> message -> message.
(**
Three mutually inductively defined relations:
- [send Y m] when [Y] send a message [m] encodes the protocol
-- A --> B : {NA,A} pk(B)
-- B --> A : {NA,NB,B} pk(A)
-- A --> B : {NB} pk(B)
The intruder [I] can send any message that (s)he knows;
- [receive Z m] when [Z] receive the message m
(ie, the message was sent by someone);
- [known m] when the message [m] is known from [I], ie
it was intercepted by [I] or deducible from informations received by [I].
*)
Section Protocol_without_flaw.
Variable X:agent.
Inductive send : agent -> message -> Prop :=
init : send A (Enc (P (Nonce (A,X)) (Name A)) X)
| trans1 : forall Y d,
receive B (Enc (P (Nonce d) (Name Y)) B)
-> send B (Enc (P (Nonce d) (P (Nonce (B,Y)) (Name B))) Y)
| trans2 : forall d, receive A (Enc (P (Nonce (A,X)) (P (Nonce d) (Name X))) A)
-> send A (Enc (Nonce d) X)
| cheat : forall m, known m -> send I m
with receive : agent -> message -> Prop :=
link : forall m Y Z, send Y m -> receive Z m
with known : message -> Prop :=
spy : forall m, receive I m -> known m
| name : forall a, known (Name a)
| nonce : forall Y, known (Nonce (I,Y))
| secret_KI : known (SK I)
| decomp_l : forall m m', known (P m m') -> known m
| decomp_r : forall m m', known (P m m') -> known m'
| compose : forall m m', known m -> known m' -> known (P m m')
| crypt : forall m a, known m -> known (Enc m a)
| decrypt : forall m a, known (Enc m a) -> known (SK a) -> known m.
(** ** Properties of the protocol *)
(** Invariant : approximates what is known from the intruder. *)
Inductive invknown : message -> Prop :=
base : forall a, invknown (Name a)
| nonce_to_I : forall a, invknown (Nonce (a,I))
| nonce_from_I : forall a, invknown (Nonce (I,a))
| mes : invknown (SK I)
| enc : forall m a, invknown m -> invknown (Enc m a)
| exchinit : X<>I -> invknown (Enc (P (Nonce (A,X)) (Name A)) X)
| exch1 : forall Y, Y<>I -> X=B ->
invknown (Enc (P (Nonce (A,B)) (P (Nonce (B,Y)) (Name B))) Y)
| exch1cheat : forall Y d, Y<>I -> invknown (Nonce d) ->
invknown (Enc (P (Nonce d) (P (Nonce (B,Y)) (Name B))) Y)
| exch2 : X=B -> invknown (Enc (Nonce (B,A)) B)
| invcompose : forall m m', invknown m -> invknown m' -> invknown (P m m').
Hint Constructors invknown.
(** Mutually recursive induction principle *)
Scheme receive_mut_ind := Minimality for receive Sort Prop
with known_mut_ind := Minimality for known Sort Prop
with send_mut_ind := Minimality for send Sort Prop.
(** Technical lemma for case analysis *)
Lemma I_eq_dec : forall a, a = I \/ a <> I.
destruct a; ((left; congruence) || (right; congruence)).
Qed.
(** Preservation of the invariant *)
Lemma receive_invknown : forall Y m, receive Y m -> invknown m.
intros Y m H; elim H using receive_mut_ind
with (P1 := invknown)
(P2 := fun (a:agent) => invknown);
intros; auto.
inversion H1; trivial.
inversion H1; trivial.
inversion H3.
inversion H1; auto; try congruence.
destruct (I_eq_dec X) as [H1|H1]; auto.
subst X; auto.
destruct (I_eq_dec Y0) as [He|He]; auto.
subst Y0; inversion H1; auto.
inversion H3; auto.
inversion H1.
inversion H3; auto.
apply exch1; congruence.
inversion H1; auto.
inversion H3; auto.
inversion H8; auto.
Qed.
(** Everything known can be sent and received and satisfies the invariant *)
Lemma known_invknown : forall m, known m -> invknown m.
intros; apply receive_invknown with I.
apply link with I.
apply cheat; auto.
Qed.
Hint Immediate known_invknown.
(** Everything not in the invariant is not known *)
Lemma not_known : forall m, ~ invknown m -> ~ known m.
red; intros; auto.
Qed.
(** Whatever [X] is the nonces generated by [A] for [B] and [B] for [A] stay private *)
Lemma NonceAB_unknown : ~ known (Nonce (A,B)).
intros; apply not_known; intro.
inversion H.
Qed.
Lemma NonceBA_unknown : ~ known (Nonce (B,A)).
intros; apply not_known; intro.
inversion H.
Qed.
(** Authentication : if [B] received the nonce generated by [A] then the protocol was initiated by [A] with [B] *)
Lemma protocol_ok : receive B (Enc (Nonce (B,A)) B) -> X = B.
intros H; inversion_clear H.
inversion_clear H0; trivial.
assert (invknown (Enc (Nonce (B, A)) B)); auto.
inversion H0; auto.
inversion H2.
Qed.
End Protocol_without_flaw.