# 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