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].