Appendix: ASTRAL specification of Needham-Schroeder protocol
SPECIFICATION Needham_Schroeder_Protocol GLOBAL SPECIFICATION NS_GLOBAL PROCESSES Initiator: array [ 1..NumberInitiator ] of ProcessInitiator, Responder: array [ 1..NumberResponder ] of ProcessResponder, Intruder: ProcessIntruder /* Intruder is used to model the intruder and the network */ TYPE PID: typedef i: ID ( IDTYPE ( i ) = ProcessResponder | IDTYPE ( i ) = ProcessInitiator | IDTYPE ( i ) = ProcessIntruder ) , INIT_RESP_ID: typedef i: ID ( IDTYPE ( i ) = ProcessResponder | IDTYPE ( i ) = ProcessInitiator ) , RESP_INTR_ID: typedef i: ID ( IDTYPE ( i ) = ProcessResponder | IDTYPE ( i ) = ProcessIntruder ) , INIT_INTR_ID: typedef i: ID ( IDTYPE ( i ) = ProcessInitiator | IDTYPE ( i ) = ProcessIntruder ) , RESP_ID: typedef i: ID ( IDTYPE ( i ) = ProcessResponder ) , INIT_ID: typedef i: ID ( IDTYPE ( i ) = ProcessInitiator ) , AGENT_STATE: ( idle, resp, init, commit_inter, commit_final ) , MsgKind: ( Msg_Type_1, Msg_Type_2, Msg_Type_3 ) CONSTANT PublicKey ( PID ) : Integer, NumberInitiator: Integer, NumberResponder: Integer AXIOM Forall i: PID, j: PID ( i ~= j -> PublicKey ( i ) ~= PublicKey ( j ) ) INVARIANT forall j: RESP_ID, i: INIT_ID ( ( j.state = commit_final & i = j.source ) -> i.Start ( Initiate ( j ) ) >= 0 ) END NS_GLOBAL
PROCESS SPECIFICATION ProcessInitiator LEVEL Top_Level IMPORT AGENT_STATE, PID, RESP_INTR_ID, PublicKey, Intruder, MsgKind EXPORT Initiate, state, source, to, from, pkey, nonce_a, nonce_b VARIABLE state: AGENT_STATE, pkey: Integer, nonce_a: integer, nonce_b: integer, source: PID, /* source is who started the protocol */ to: PID, from: PID, kind: MsgKind INITIAL state = idle & nonce_a = 0 & pkey = PublicKey ( self ) & nonce_b = 0 & source = self & to = self & from = self TRANSITION Initiate ( j: RESP_INTR_ID ) ENTRY [ TIME : 1 ] state = idle EXIT state = init & nonce_a = nonce_a /* get a fresh nonce */ & to = j & from = self & pkey = PublicKey ( j ) & source = self & kind = Msg_Type_1 TRANSITION Receive ( j: RESP_INTR_ID ) ENTRY [ TIME : 1 ] state = init & Intruder.to = self & Intruder.from = j & Intruder.pkey = PublicKey ( self ) & Intruder.nonce_a = nonce_a /* the nonce is fresh */ & Intruder.source = self & Intruder.kind = Msg_Type_2 EXIT state = commit_inter & nonce_b = Intruder.nonce_b & pkey = PublicKey ( j ) & to = j & from = self & kind = Msg_Type_3 & source = self END Top_Level END ProcessInitiator
PROCESS SPECIFICATION ProcessResponder LEVEL Top_Level IMPORT INIT_INTR_ID, PublicKey, AGENT_STATE, PID, Intruder, MsgKind EXPORT state, source, nonce_a, nonce_b, pkey VARIABLE state: AGENT_STATE, pkey: Integer, nonce_a: Integer, nonce_b: Integer, source: PID, to: PID, from: PID, kind: MsgKind INITIAL state = idle & nonce_a = 0 & to = self & from = self & source = self & nonce_b = 0 & pkey = PublicKey ( self ) TRANSITION Respond ( i: INIT_INTR_ID ) ENTRY [ TIME : 1 ] state = idle & Intruder.pkey = PublicKey ( self ) & Intruder.to = self & Intruder.from = i & Intruder.kind = Msg_Type_1 EXIT state = resp & nonce_b = nonce_b /* get a fresh nonce */ & pkey = PublicKey ( Intruder.source ) & nonce_a = Intruder.nonce_a & to = i & from = self & source = Intruder.source & kind = Msg_Type_2 TRANSITION Receive ( i: INIT_INTR_ID ) ENTRY [ TIME : 1 ] state = resp & Intruder.pkey = PublicKey ( self ) & Intruder.nonce_b = nonce_b /* the nonce is fresh */ & Intruder.to = self & Intruder.from = i & Intruder.kind = Msg_Type_3 EXIT state = commit_final & source = Intruder.source & pkey = PublicKey ( self ) & from = self & to = i END Top_Level END ProcessResponder
PROCESS SPECIFICATION ProcessIntruder LEVEL Top_Level IMPORT INIT_ID, RESP_ID, INIT_RESP_ID, INIT_INTR_ID, RESP_INTR_ID, PublicKey, AGENT_STATE, PID, MsgKind, Initiator.state, Responder.state EXPORT source, nonce_a, nonce_b, pkey, to, from VARIABLE ifknow_nonce_a ( INIT_RESP_ID ) : Boolean, ifknow_nonce_b ( INIT_RESP_ID ) : Boolean, know_nonce_a ( INIT_RESP_ID ) : Integer, know_nonce_b ( INIT_RESP_ID ) : Integer, pkey: Integer, nonce_a: Integer, nonce_b: Integer, source: PID, to: PID, from: PID, kind: MsgKind, status ( INIT_RESP_ID ) : AGENT_STATE INITIAL forall i: INIT_RESP_ID ( ifknow_nonce_a ( i ) = False & ifknow_nonce_b ( i ) = False ) & source = self & to = self & from = self & kind = Msg_Type_1 & pkey = PublicKey ( self ) & forall i: INIT_RESP_ID ( status ( i ) = idle ) TRANSITION Attack_Init ( i: INIT_ID, j: RESP_ID ) /* message is to the intruder, decrypt and know nonce_a */ ENTRY [ TIME : 1 ] i.pkey = PublicKey ( self ) & i.kind = Msg_Type_1 & ~ifknow_nonce_a ( i ) EXIT ifknow_nonce_a ( i ) Becomes True & know_nonce_a ( i ) Becomes i.nonce_a /* produce a message with known nonces */ EXCEPT [ TIME : 1 ] ifknow_nonce_a ( i ) & ifknow_nonce_b ( j ) EXIT pkey = PublicKey ( i ) & nonce_a = know_nonce_a' ( i ) & nonce_b = know_nonce_b' ( j ) & from = self & to = i & kind = Msg_Type_2 & source = i /* message is to the intruder, decrypt and know nonce_b */ EXCEPT [ TIME : 1 ] i.kind = Msg_Type_3 & i.pkey = PublicKey ( self ) & ~ifknow_nonce_b ( i ) EXIT ifknow_nonce_b ( i ) Becomes TRUE & know_nonce_b ( i ) Becomes i.nonce_b TRANSITION Attack_Resp ( j: RESP_ID, i: INIT_ID ) /* message is to the intruder, decrypt and know nonce_b */ ENTRY [ TIME : 1 ] j.pkey = PublicKey ( self ) & j.kind = Msg_Type_2 & ~ifknow_nonce_b ( j ) EXIT ifknow_nonce_b ( j ) Becomes TRUE & know_nonce_b ( j ) Becomes j.nonce_b /* nonce_a known, so produce Msg_Type_1 message */ EXCEPT [ TIME : 1 ] ifknow_nonce_a ( i ) EXIT pkey = PublicKey ( j ) & nonce_a = know_nonce_a' ( i ) & source = i & to = j & from = self & kind = Msg_Type_1 /* nonce_b known, so produce Msg_Type_3 message */ EXCEPT [ TIME : 1 ] ifknow_nonce_b ( i ) EXIT pkey = PublicKey ( j ) & to = j & from = self & source = i & kind = Msg_Type_3 & nonce_b = know_nonce_b' ( i ) /* nonce_b known, so produce Msg_Type_3 message */ EXCEPT [ TIME : 1 ] ifknow_nonce_b ( j ) EXIT pkey = PublicKey ( j ) & to = j & from = self & source = i & kind = Msg_Type_3 & nonce_b = know_nonce_b' ( j ) TRANSITION Relay ( i: INIT_RESP_ID ) ENTRY [ TIME : 1 ] i.pkey ~= PublicKey ( self ) & status ( i ) ~= i.state EXIT status ( i ) BECOMES i.state & kind = i.kind & source = i.source & to = i.to & from = i.from & pkey = i.pkey & nonce_a = i.nonce_a & nonce_b = i.nonce_b TRANSITION Replay ( i: INIT_ID, j: RESP_ID ) /* direct the message to responder j */ ENTRY [ TIME : 1 ] i.pkey ~= PublicKey ( self ) & i.to = self & status ( i ) ~= i.state EXIT status ( i ) Becomes i.state & kind = i.kind & source = i.source & to = j & from = self & pkey = i.pkey & nonce_a = i.nonce_a & nonce_b = i.nonce_b /* direct the message to initiator i */ EXCEPT [ TIME : 1 ] j.pkey ~= PublicKey ( self ) & j.to = self & status ( j ) ~= j.state EXIT status ( j ) Becomes j.state & kind = j.kind & source = j.source & to = i & from = self & pkey = j.pkey & nonce_a = j.nonce_a & nonce_b = j.nonce_b END Top_Level END ProcessIntruder END Needham_Schroeder_Protocol