Library NSPK
Needham-Schroeder protocol
simplified bversion without a server for distributing public keys
- 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} 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.
A global parameter X represents the agent with which A initiates the protocol
A and B follow the protocol
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) (Nonce (B,Y))) Y)
| trans2 : forall d, receive A (Enc (P (Nonce (A,X)) (Nonce d)) 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.
End Protocol_with_flaw.
Hint Resolve init trans1 link secret_KI
decomp_l decomp_r compose cheat spy name.
The protocol can end with B receiving the message (Enc (Nonce (B,A)) B)
while the protocol was initiated with I.
The nonce generated by B for A is made public