Library NSPK1

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.

Preservation of the invariant
Lemma receive_invknown : forall Y m, receive Y m -> invknown m.

Everything known can be sent and received and satisfies the invariant
Lemma known_invknown : forall m, known m -> invknown m.
Hint Immediate known_invknown.

Everything not in the invariant is not known
Lemma not_known : forall m, ~ invknown m -> ~ known m.

Whatever X is the nonces generated by A for B and B for A stay private
Lemma NonceAB_unknown : ~ known (Nonce (A,B)).

Lemma NonceBA_unknown : ~ known (Nonce (B,A)).

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.

End Protocol_without_flaw.