Obviously, the constructor Says expresses sending a messages. Says A B X states thatAattempts to send a message X to B.
TheGetsconstructor, explicitly expressing message reception, is an extension to eventby G.Bella [5] in order to model agent’s knowledge via message reception.
Gets B X expresses B’s reception of a message X. It only indicates that the message was previously sent, butB does not have any knowledge about who is the sender. In Paulson’s work [26], this case is expressed as SaysA0 B X with-out the Gets constructor. In this way, the sender is stated as A0 which is not used elsewhere, becauseBcannot get to know the real sender of the messageX.
However, the extension of Getscan improve the readability of the specifications of protocols and security properties.
NotesA Xexpresses that the agentAinternally storesX which is a part of the message he received. This means the event is only known byAhimself, as long asAis uncompromised. Otherwise, ifAis a bad agent, the eventNotesA X is also visible to the spy.
3.1.4 Event Traces
As mentioned above, the history of agents’ actions is formalized as a list of events, namely a trace. When an event has taken place, the existing trace is then extended with the new event. A trace is a list of events in reverse order.
So the new event is inserted to the head of the list. In Isabelle syntax,ev#evs expresses the traceevsis extended with the new eventev.
Moreover, given a traceevs,setevsrepresents the set of all events in the trace, that is, all the events that have occurred. According to Isabelle’s Logic, the functionsetmaps a list to the set that consists of all elements from the list.
Therefore, given ev∈ setevs, it is indicated that the event ev has taken place on traceevs.
3.2 Agent’s Knowledge
In order to model agents’ knowledge inductively, the initial knowledge of agents is required to be specified.
3.2.1 Initial Knowledge
To specify the initial knowledge of agents before the protocol starts, the function initStateis declared as follows.
consts initState :: "agent => msg set"
The function initState maps an agent’s name to the set of messages that are known by the agent before the running of the protocol. So the notation init-State A expresses the initial knowledge of the agent A. In a symmetric key setting, for each type of agents, the initial knowledge of the agent is defined respectively as follows.
primrec
initState Server:
"initState Server = (Key ‘ range shrK)"
initState Friend:
"initState (Friend i) = Key (shrK(Friend i))"
initState Spy:
"initState Spy = (Key ‘ shrK ‘ bad)
According to Isabelle’s logics, a function’s range is the set of values that the function can take on, in other word, the image of the universal set under that function. Therefore, range shrKrepresents the set of all shared keys. And the notation f ‘ A represents the image of the set A under the function f [25].
In this way, the above definition of agents’ initial knowledge turns to be clear.
The server’s initial knowledge contains the shared keys of all the agents on the network, that is, all long-term keys on the network. The initial knowledge of a friendly agent is his own long-term key that is shared with the server. And the spy’s initial knowledge contains shared keys of all compromised agents, includ-ing his own shared key, of course.
3.2.2 Modelling Agent’s Knowledge
The function knows is introduced to describe an agent’s knowledge on some trace.
consts knows :: "agent => event list => msg set"
The notation knowsA evs represents the set of message that the agentA can
3.2 Agent’s Knowledge 25
obtain based on the traceevs. This knowledge is defined as follows.
primrec
knows Nil: "knows A [] = initState A"
knows Cons:
if A’∈bad then insert X (knows Spy evs) else knows Spy evs) else
(case ev of Says A’ B X =>
if A’=A then insert X (knows A evs) else knows A evs
| Gets A’ X =>
if A’=A then insert X (knows A evs) else knows A evs
| Notes A’ X =>
if A’=A then insert X (knows A evs) else knows A evs))"
• At the beginning, any agent’s knowledge is just his initial knowledge.
• About the spy’s knowledge, he knows every message sent over the network no matter who is the sender or the receiver. And the spy also knows what is noted by every compromised agent. Notice that aGetsevent for message reception does not extend the spy’s knowledge because theSaysevent for sending that message did so already.
• For an agent other than the spy, he knows every message sent by himself, and he knows every message he received. Every note by that agent on the trace is also included in the agent’s knowledge.
The modelling of agents’ knowledge was introduced by G. Bella [5]. In Paul-son’s original version [26] of the inductive approach, only the spy’s knowledge was modelled. A function spies is used to specify the spy’s knowledge. The notation spiesevs represents the set of message that the spy can see based on the traceevs.
spies[ ],initState Spy
spies((SaysA B X)#evs),{X} ∪spiesevs spies((NotesA X)#evs),
{X} ∪spiesevs ifA∈bad spiesevs otherwise
In the current logic library of Isabelle 2005 [1], the basic theories for protocol verification have already been updated with G. Bella’s extension [5] of agents’
knowledge and message reception. However, the use of spies is still retained for compatibility, as the syntax for spies stays in the theory. For simple key-distribution protocols, Paulson’s original syntax would be sufficient for analysis of the security properties. In this thesis, we adopt the original syntax in mod-elling and analyzing the protocol, and then update the protocol model with message reception and agent’s knowledge.