Library NSPK1
Needham-Schroeder protocol
simplified bversion without a server for distributing public keys
version without flaw
- 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)
- 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.
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
Preservation of the invariant
Everything known can be sent and received and satisfies the invariant
Everything not in the invariant is not known
Whatever X is the nonces generated by A for B and B for A stay private
Authentication : if B received the nonce generated by A then the protocol was initiated by A with B