next up previous
Up: On Searching for Known Previous: References

Appendix: Specification of the ESP Protocol

fs(1):host(A) --> W::.
fs(2):iv(U,N) --> W::.
fs(3):key(U,V) --> W::.
fs(4):header(U,V,Type,Num) --> W::.
fs(6):mess(U,V,TS,Num) --> W::.
fs(7):plus(Num) --> W::.
fs(8):ts(U,N) --> W::.
fs(9):user(A,H) --> W::.
fs(10):spi(U,V) --> W::.

op(2):ecbc(X,Y,Z) --> W:::pen.
op(3):dcbc(X,Y,Z) --> W:::pen.


atom(1):honest --> W:.
atom(2):dishonest --> W:.
atom(3):notsent --> W:.
atom(4):nil --> W:.
atom(5):one --> W:.
atom(6):short --> W:.
atom(7):long --> W:.
atom(8):word --> W:.
atom(9):header --> W:.


rr(1):ecbc(K,IV,dcbc(K,IV,Z)) => Z.
rr(3):dcbc(K,IV,ecbc(K,IV,Z)) => Z.

known: host(A), user(A,H), header(U,V,Type,Num),
mess(user(C,dishonest),V,TS,Num),
notsent, spi(H1,H2),
plus(Num).

/*host(A) sends message from host user user(C,honest) to user(D,H)
on host(B)
message is
spi(host(A),host(B)), [SA denotes the security association]
header(user(C,honest),user(D,H)) [indicates that the header says
    who the message is from and who it is
    to, among other things]
data(user(C,honest),user(D,H),ts(host(A),N))
   [denotes actual encrypted data sent
   the ts(host(A),N) is a syntactic device to ensure
   uniques of encrypted data (we are assuming that
   encrypted data is unique]*/



rule(1)
If:
count(host(A)) = [N],
then:
count(host(A)) = [s(N)],
lfact(host(A),N,host_encryptstate,s(N)) = 
  [host(B),user(C,honest),user(D,H),
 ecbc(key(host(A),host(B)),
  iv(host(A),N),header(user(C,honest),user(D,H),Htype,one)),
 header,Htype,one],
intruderlearns([spi(host(A),host(B)),iv(host(A),N),
 ecbc(key(host(A),host(B)),
  iv(host(A),N),
  header(user(C,honest),user(D,H),Htype,one))]),

EVENT:
event(host(A),N,host_firstheader,s(N)) = [host(B),user(C,honest),user(D,H),
iv(host(A),N)].

rule(2)
If:
count(host(A)) = [T],
lfact(host(A),N,host_encryptstate,T) = [Host,user(C,honest),V,CT,header,long,Num],
not(Num = plus(Num1)),
then:
count(host(A)) = [s(T)],
lfact(host(A),N,host_encryptstate,s(T)) = [Host,user(C,honest),V,
 ecbc(key(host(A),Host),CT,header(user(C,honest),V,long,plus(Num))),header,
 long,plus(Num)],
intruderlearns([ecbc(key(host(A),Host),CT,header(user(C,honest),V,Htype,plus(Num)))]),
EVENT:
event(host(A),N,host_secondheader,s(T)) = [Host,user(C,honest),V,CT,Num].

rule(3)
If:
count(host(A)) = [T],
lfact(host(A),N,host_encryptstate,T) = [Host,user(C,honest),V,CT,Type,Htype,Num],
not(Num = plus(plus(plus(Num1)))),
then:
count(host(A)) = [s(T)],
lfact(host(A),N,host_encryptstate,s(T)) = [Host,user(C,honest),V,
 ecbc(key(host(A),Host),CT,mess(user(C,honest),V,ts(host(A),T),Num)),
 word,Htype,plus(Num)],
intruderlearns([ecbc(key(host(A),Host),CT,mess(user(C,honest),V,ts(host(A),T),Num))]),
EVENT:
event(host(A),N,host_messageword,s(T)) = [Host,user(C,honest),V,CT,Num].

/*Rules describing intruder encrypting a message*/

rule(4)
If:
count(host(A)) = [N],
intruderknows([user(C,dishonest),user(D,H)]),
then:
count(host(A)) = [s(N)],
lfact(host(A),N,host_encryptstate,s(N)) = 
  [host(B),user(C,dishonest),user(D,H),
 ecbc(key(host(A),host(B)),
  iv(host(A),N),header(user(C,dishonest),user(D,H),Htype,one)),
 header,Htype,one],
intruderlearns([spi(host(A),host(B)),iv(host(A),N),
 ecbc(key(host(A),host(B)),
  iv(host(A),N),
  header(user(C,dishonest),user(D,H),Htype,one))]),
EVENT:
event(host(A),N,host_firstbadguyheader,s(N)) = [host(B),user(C,dishonest),user(D,H),
    iv(host(A),N)].

rule(5)
If:
count(host(A)) = [T],
intruderknows([header(user(C,dishonest),V,Htype,plus(one))]),
lfact(host(A),N,host_encryptstate,T) = [Host,user(C,dishonest),V,CT,header,long,Num],
not(Num = plus(Num1)),
then:
count(host(A)) = [s(T)],
lfact(host(A),N,host_encryptstate,s(T)) = [Host,user(C,dishonest),V,
 ecbc(key(host(A),Host),
    CT,header(user(C,dishonest),V,long,plus(Num))),header,Htype,plus(Num)],
intruderlearns([ecbc(key(host(A),Host),CT,header(user(C,dishonest),V,long,plus(Num)))]),
EVENT:
event(host(A),N,host_badguysecondheader,s(T)) = [Host,user(C,dishonest),V,CT,Num].

rule(6)
If:
count(host(A)) = [T],
intruderknows([X]),
lfact(host(A),N,host_encryptstate,T) = [Host,user(C,dishonest),V,CT,Type,Htype,Num],
not(Num = plus(plus(plus(Num1)))),
then:
count(host(A)) = [s(T)],
lfact(host(A),N,host_encryptstate,s(T)) = [Host,user(C,dishonest),V,
 ecbc(key(host(A),Host),CT,X),
 word,Htype,plus(Num)],
intruderlearns([ecbc(key(host(A),Host),CT,X)]),
EVENT:
event(host(A),N,host_badguymessageword,s(T)) = [Host,user(C,dishonest),V,CT,Num].


/*Host decrypts message*/

rule(7)
If:
count(host(A)) = [N],
intruderknows([spi(host(B),host(A)),IV,X]),
then:
count(host(A)) = [s(N)],
lfact(host(A),N,host_decryptstate,s(N)) = [host(B),nil,nil,
 X,dcbc(key(host(B),host(A)),IV,X),header,one],
EVENT:
event(host(A),N,host_first,s(N)) = [host(B),IV,X].


rule(8)
If:
count(host(A)) = [T],
intruderknows([X]),
lfact(host(A),N,host_decryptstate,T) = [host(B),nil,nil,
 Y,header(user(C,H),user(D,J),long,one),header,one],
not(Num = plus(Num1)),
then:
count(host(A)) = [s(T)],
lfact(host(A),N,host_decryptstate,s(T)) = [host(B),user(C,H),user(D,J),
 X,dcbc(key(host(B),host(A)),Y,X),header,plus(one)],
EVENT:
event(host(A),N,host_continuedheader,s(T)) = [host(B),user(C,H),
 user(D,J),Y,X].

rule(9)
If:
count(host(A)) = [T],
intruderknows([X]),
lfact(host(A),N,host_decryptstate,T) = [host(B),user(C,H),user(D,J),
 Y,header(user(C,H),user(D,J),long,plus(one)),header,plus(one)],
then:
count(host(A)) = [s(T)],
lfact(host(A),N,host_decryptstate,s(T)) = [host(B),user(C,H),user(D,J),
 X,dcbc(key(host(B),host(A)),Y,X),word,plus(plus(one))],
EVENT:
event(host(A),N,host_decryptedfirstword,s(T)) = [host(B),user(C,H),
 user(D,J),X,Y].

rule(10)
If:
count(host(A)) = [T],
intruderknows([X]),
lfact(host(A),N,host_decryptstate,T) = [host(B),nil,nil,
 Y,header(user(C,H),user(D,J),short,one),header,one],
then:
count(host(A)) = [s(T)],
lfact(host(A),N,host_decryptstate,s(T)) = [host(B),user(C,H),user(D,J),
 X,dcbc(key(host(B),host(A)),Y,X),word,plus(one)],
EVENT:
event(host(A),N,host_decryptedfirstword,s(T)) = [host(B),user(C,H),
 user(D,J),X,Y].




rule(11)
If:
count(host(A)) = [T],
intruderknows([X]),
lfact(host(A),N,host_decryptstate,T) = [host(B),user(C,H),user(D,J),
 Y,Z,word,Num],
not(Num = plus(plus(plus(Num1)))),
then:
count(host(A)) = [s(T)],
lfact(host(A),N,host_decryptstate,s(T)) = [host(B),user(C,H),user(D,J),
 X,dcbc(key(host(B),host(A)),Y,X),word,plus(Num)],
EVENT:
event(host(A),N,host_decryptedword,s(T)) = [host(B),user(C,H),
 user(D,J),X,Y].





rule(12)
If:
count(host(A)) = [T],
lfact(host(A),N,host_decryptstate,T) = [host(B),user(C,H),user(D,dishonest),
 X,Y,word,Num],
then:
count(host(A)) = [s(T)],
intruderlearns([Y]),
EVENT:
event(host(A),N,host_revealedword,s(T)) = [host(B),user(C,H),
 user(D,dishonest),X,Y].