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