Non-monotonic Properties for Proving Correctness in a Framework of
Compositional Logic
Koji Hasebe

Mitsuhiro Okada

Department of Philosophy, Keio University
2-15-45
 Mita, Minato-ku, Tokyo 108-8345, Japan
hasebe,mitsu  @abelard.flet.keio.ac.jp
June 12, 2004

Abstract
Following up our previous work [9], we distinguish the monotonic properties and the non-monotonic ones
in our inference system based on the framework of compositional logic, and give the way to include somenon-monotonic properties. As an example, we present a correctness proof of Challenge Response protocol, andexplain how such properties can be used in more powerful derivations. We also give a semantics based on thenotion of trace, and present a soundness proof of our inference system including non-monotonic properties.

1 Introduction
Compositional logic (originally introduced by Durgin-Mitchell-Pavlovic [6] and Datta-Derek-Mitchell-Pavlovic[3, 4]) is an inference system based on Floyd-Hoare style logical framework for proving protocol correctness. Bymeans of this framework, a protocol is considered as a program, and a statement “from a principal  ’s viewpoint,a general property  holds
at the end of his/her protocol action  ” can be represented as a formula of the form  (or of the form   in [3, 4]). One of the most advantageous points of this framework is its compositional
approach for reasoning about a compound protocol: in order to prove a property about a compound protocol we
can reuse already established properties about its components.
In our previous work [9], we presented a way for making more explicit the compositionality property ofthis framework by introducing a notion of primitive actions in a role (i.e., sending, receiving or generating actions). While in [6, 3, 4] an assumption about a principal’s honesty is represented as implication of the form
 (which means “if principal is honest, then  holds”),inour framework such assumption(called honesty assumption) is represented by the predicates of the form
(where ! is a sequence ofprimitive actions in a role performed by ) in the left hand side of a sequent style assertion. In a proving processof a property, these honesty assumptions are composed by combining the usual contraction rule of the sequentcalculus and the following weakening rule (analogous to the weakening rule of the traditional logic).

 "  '&)(+*  ,  , $# %# %- Weakening "  '&)(+*  ,  , , 
%
%
%
%
%
%
$

.
#

#

#
#




/ This work was partly supported by Grants-in-Aid for Scientific Research of MEXT, Center of Excellence of MEXT on Humanity
Sciences (Keio University), the Japan-US collaborative research program of JSPS-NSF, Oogata-kenkyuu-jyosei grant (Keio University)and Global Security Center grant (Keio University). The first author was also supported by Fellowship for Japanese Young Scientists fromJapan Society for the Promotion of Science.

1

(



 

(This means that, “from  ’s view,
with ’s honesty on 0#  % after  ’s performance, ,  if a property  is derived from
(



%
#
,
then

is
also
derivedfromwith’s honesty on 0#. % % #  % after  ’s performanceof thesequenceofactions
, , , ,of # % % # % , for any addition  % % and % % in the roles”.) In [9], we showed that this type of inferences is used forproving a property about a compound protocol, directly composing proofs of its components.
When we can freely apply the weakening rule to  , we call  a monotonic property 1 . Freshness, sending-fact,
receiving-fact are examples of monotonic properties. In [9], we took as an example a set of monotonic properties,
and demonstrated that such an inference system has enough power to prove (non-injective) agreement property (inthe sense of Woo-Lam [10]) of some protocols, even if we do not use logical negation, nested implications, or any
temporal operators as introduced in [3, 4] 2 .
However, if we want to prove a property stronger than the agreement property, we need some non-monotonic
properties. In this paper, we give the way to include some non-monotonic properties in our framework of compositional logic. As an example, we aim at proving matching conversations of Challenge Response Protocol [5]which was also shown in [3, 4]. This property is stronger than the agreement property, because we need to prove
additional properties about the ordering of actions performed by the different principals. To prove this property,
7698 ;:<. We show a proof of this property in this extended syswe introduce a non-monotonic property “ 13254
tem only by adding a few restrictions on the weakening rules previously shown and on the inference rules on aprincipal’s honesty (called honesty inferences). In particular, we do not use logical negation, nested implicationand temporal operators, which are used in the original proof of [3, 4].
In this paper, we use the following notations (cf. Appendix A of [9]). The letters = , > , ? ,. . . ( , , @ ,. . . ,& &BBBC& & &BBB
resp.) are constants (variables , resp.) of principal’s names. The capital letters A A %H&)H &BBBC&)H &)H &BBB& AE&D BBAG
B& F & and&BBB
K% &L &BBBC&LD  &LF  &BBare
B constants of keys and of nonces, respectively, while the& small&BBlettersBN&& I IJ%&BBB I D I F%
andare variables of the same sorts as above. The letters M M %are used to
M D M FD F
&BBBN&E
M
US
T
denote messages, and ONM+PQ is the encryption of M with key A , and R M D
is the concatenation of mes&BBBC&
sages M D
MES . We also introduce MWVXM % to represent the subterm relation as a meta symbol.
The rest of this paper is organized as follows. In Chapter 2, we shall review the inference system introduced in[9]. In Chapter 3, we shall show how to include non-monotonic properties in the system. Moreover, as an example,
we prove the matching conversations of CR protocol which cannot be proved only by the monotonic properties. In
Chapter 4, we shall give a semantics based on the notion of trace, and sketch out a soundness proof of the extended
system. In Chapter 5, we shall present our conclusions and some further issues.

2 Inference system
2.1 The Language



 & 

mQ

Predicates of our inference system are as follows: ZY<[]\3[^7_a`5[cb , d^)[)e'[f9g"[cbhM 3 , ibN[]\kjbhM , lA  I , n o
qpi% . While the first three predicates
, 134
and
by  ), the rest of& , &7roare&.s&called
BBB"& action& &Bpredicates
BB& & &(performed
BBB
K

%
;

%
%


are used to denote action
them are called non-action predicates. The letters DF& , &7r &.s &BBB& &BBB& & &BBB%
predicates (also ht
to denote action predicates performed by  ) andare nont t t
D F
action predicates. All those predicates except for equality are chosen from the BAN logic predicates [1]. Equality
1

This notion of monotonic property is essentially the same as persistent property in the sense of [6, 3, 4], except that the notion ofmonotonicity is related not only to weakening for protocol actions (described in the square bracket “[ ]”) but also to weakening for honesty
assumptions.
2
The reason why we do not need logical negation nor nested implications (nor, disjunctions in the right hand side of a sequent) is that
we restrict the honesty inferences. By this restriction, in our framework each sequent is expressed by a Horn-clause, however it is trade-off
against some kinds of inferences on honesty. (See also Section 5.)/
3
We distinguish two kinds of “u'v)wxvLy{zNv.| ”: the simple receiving/ and the receiving with decryptions. }G~5 '9) h means that“ } receives a term  and decrypts the indicated subterm )    of  . For a more formal description, instead of using  , we could
introduce a new predicate NvLwxu.)| and describe it by }~5 '  }x~53)     .

2

is used for explicit treatment of substitutions. As we have mentioned in Section 1, all those predicates except forCN;: have monotonic properties (i.e., properties independent of the weakening rules for principal’s actions andfor honesty assumptions)4 .
As logical connectives, we introduce only usual conjunction (denoted by “,”) and non-commutative conjunction (denoted by “;”). Our intention is to use non-commutative conjunction to represent a sequence of principals’
actions, implicitly treated in [9]. While in [3, 4] some temporal operators are used to reason about the ordering of actions, we get rid of any temporal operators: the orderings are directly derived from the axioms, using
inference rules presented in Appendix. We introduce the vector notation such as  to denote a sequence (i.e.,
non-commutative conjunct),  p , of action, predicates.
p ,<¤ We also introducep§¦&BBsome
BC&L notions related to p a sequence
BBB of action. We say o¡¢(
for some ¥ . For a sequence##.S andD #£££# S ) if ¡
D

¤
,
,
,
,
& ¤


p

B

B
B

for  ¡ 
for all  ¡ ¢  and if¢  , we denote  ¡©¨G« ª  if 2 ¨ ¥  . For  and (DN# # S ), if  ¡ ¢

¤®­
¤
,
,
¬ & ¤
 B{


;¡  ¢  ;¡ ¨ « ª ;¡ ¨ ¯ ª  , we say is an extension of  and denote it by ±° .
calculus style assertion. The basic form of assertion is as follows (where Our inference ¤ system uses &aBBsequentBN&'¡ may be in the list of ).

 &BBBC& , ²CCN '&BBBC&) CN ,  '&.³´*  r  t{ µ

&BBBN&' is a sequence
Here each of  tof action predicates performed by 
, respectively, which repr
resents a part of his/her role, and is a sequence of concrete actions performed by = . 5 Each of the letters& &BBB& & &BBB %
³ D  F
is a sequence (i.e., non-commutative conjunct) of action predicates, or a single non-action&BBB& 
is of the form  DS. Each predicate of the form
ht represents “a principal  honpredicate.

estly follows a part of role  ”. We call it  ’s honesty assumption. To formalize such assumptions on honesty, in²CCN  which means “principal  is honest”. On the other hand, our[6, 3, 4], they introduce the predicate
intention is to make more explicit the compositionality of honesty assumptions: we separate each honest principal’s role into his/her primitive actions, and construct a composed proof by using some basic natural logical rules.
(The details of the composing process were presented in [9].)CN 
If t consists of a sequence of primitive actions qt D #k£££¶#.oSt , we can consider the predicate
ht as²CCN   t D #£££C#
 St , which is a conjunct of non-commutative
an abbreviation of
conjunction.
&BBBN&'
honestly follow
Therefore, the intuitive meaning
 &BBBC& ,  of the sequent previously introduced ³ is “if principals  , respectively, and if somer properties hold, then after = performs a sequence
the parts of their roles  t
rof concrete
actions
,
holds
from

= ’s viewpoint”. (Here may be empty. In such case we often use  , insteadof   .)  & h & 
Finally, we introduce the postfix notation <Iin order to denote the listsofprincipalnames

(list of
&BBBC&h & variables 0D· ), and the lists of variables of nonces and session keys I (as variables). Substitutions are
represented in terms of this notation.
2.2 Axioms and inference rules
Our inference system consists of the following four classes (I)-(IV) of axioms and of inference rules. (The complete list is also presented in Appendix.)(I) Logical inferences with equality: As logical inferences, we use some structural rules (I-1) (weakening, contraction, exchange rules of the left hand side, and cut rule) and equality inference rules (I-2), and substitution rules
As we shall see in the explanation of the Matching rule of the honesty inferences below, predicate “ |LvL¸a| ” is monotonic w.r.t. theweakening for concrete actions, however it is non-monotonic w.r.t. the weakening for honesty assumptions. In other words, this predicate
is non-monotonic in the sense of our terminology, however it is “persistent” in the sense of [6, 3, 4].
5Note that for describing a sequence of action, while compositional logic of [6, 3, 4] uses the cord calculus, we describe it by thepredicates previously shown.
43

(I-3). These are chosen from the traditional first order logic with equality. We also introduce some inference rules
for non-commutative conjunction (I-4).
(II) Action properties axioms: These are composed of the axioms about actions and the axioms for relationshipbetween properties in the sense of [6]. Our proposed axioms are listed in (II-1) and (II-2), respectively. (Here,
7698 ;:<
axioms including non-monotonic property 13254, which is introduced in Section 3, are marked with thesymbol “ ¹ ”.) However, our framework does not depend on any specific set of axioms in this class.
(III) Honesty inferences:For deriving ’s other actions from  ’ viewpoint,  may assume ’s honesty and may use his/her own knowl
edge about ’s role in the protocol. For example, if  knows that has sent the message M in a current run,

and assumes that is honest, then  can derive ’s previous action, because should not have sent the message
M if he/she has not already performed all the previous actions of his/her role. For formalizing such inferences,compositional logic in [6, 3, 4] uses a special inference (called honesty rule) for deriving a conclusion of the form
 . On the other hand, in our system, inferences on honesty are formalized by the three kinds ofinference rules: Substitution (III-1), Matching (III-2) and Deriving another action (III-3). These are called honesty
inferences. For example, the following inference rule is the Matching rule.

,r³º*   ,   r t #b[]\3jb!M #³»&)²]
& q*   ,  r  Hon(Match)bN[]\kjbhM % M
 t # bN[]\kjbhM % #(Here and are non-commutative conjuncts of some action predicates, respectively, (where each of them may
be empty), and MWVXM % .)
The intended meaning of this inference rule is that “if  assumes that is honest and follows the sendingaction “ b[]\3jbKM % ”, and if  knows that sends a message M containing M % ”, then we can conclude that “ knows that has sent M % ”. This inference holds whenever the additional condition is satisfied such that “ ’shonesty assumption does not include any other sending action of a message which includes M as a subterm”. Thismeans that the formula bN[]\kjbhM % appearing in the lower sequent is non-monotonic. Thus, to keep our systemmonotonic, we restrict all applications of honesty inferences and of weakening rule for honesty assumptions(explained in the next item (IV)) so as to preserve this condition. More formally, we extend the language by²] & ²] 
introducing a new predicate
 M (here previously defined can be regarded as a special
case such that M is empty), and all applications of the honesty inferences and the weakening rule for honesty
¼L
assumptions are restricted by the following condition (denoted by ).

¼L

²]

&

bN[]\kjb!M% M andBoth predicatesappear in the left hand side of the lower sequent.

²]


bN[]\kjbhME% % (with M

V½ME% % ) do not(IV) Weakening rules for actions and for honesty assumptions: We now introduce the weakening rules forhonesty assumptions and the weakening rule for concrete actions. All the applications of these weakening rules
¼L
are restricted so as to satisfy thecondition of Matching rule of honesty inferences.
If we introduce a non-monotonic predicate, as we shall explain in the next section, some additional condition
should be necessary. In other words, our choice of predicates is one of the simplest formalism with respect to theweakening rules.
Finally we point out a limitation of our system. For a protocol including duplications of the same actions, wecannot distinguish one from another in our logic, because our logic does not explicitly deal with position during
the run of a protocol. In this paper we consider only protocols which does not include any duplication.

43 Introducing a non-monotonic property in correctness proofs
In this section, we give the way to include some non-monotonic properties in our inference system presented inx6 8 ;: 
the previous section. In Section 3.1, as an example, we introduce a non-monotonic predicate “ 1324”
which is used to reason about some ordering of actions, and explain some additional restrictions on the honesty
inferences and the weakening rules. In Section 3.2, we show a proof of matching conversations of Challenge
Response Protocol [5]. This property was already proved in [3, 4], however logical negation, nested implications
and temporal operators are not used in our proof.

3.1 Inferences for non-monotonic properties

CCn

In order to prove our aimed property, whereas the predicate ¾¿4
is used in [3, 4], we introduce a new pred7698 ;:<;:  &Loicate 13254(also denoted by 1
for readability). ²À.bN[]\kjb Mmeans “ sends a message M


+
M
%
containing as a subterm, and  does not send any othermessagecontaining
before the sending of M ”.
*  &Lo
Clearly, this predicate is non-monotonic, because if $#. % % #  % +À'b[]\3jb Mholds, where  % % is  ’s sendingof M , and if we insert another  ’s sending of M²% with VÁMÂ% before % % , then this predicate becomes false under
this weakened assumption (in square bracket “[ ]”). As this observation tells us, if we introduce a non-monotonic
predicate in our framework, we must restrict all applications of the weakening rules (both for honesty assumptions
and for actions) and all the honesty inferences ((III-1)-(III-3)) by the following additional conditions (denoted by¼L¼L 6).

 ¼L¼L
 ,  r
s
³ '&BBBC&For eachsequence
,
,
and
for
each
(which appears in ) in the lower sequentt
²CCN , '&.³´*  r   &Lo L t, it is no extension of a sequence of the form Ãb[\kjbKM % # +À'b[\kjb M&(with VXM M % ) for any  .

C SomeN;:  non-monotonic properties are useful for reasoning about ordering of actions. Actually in the case of, the order between different principals’ actions can be derived by the additional inference rule and axiom
1
as follows.
Firstly Sends:²CCN '&BBBC&)  ,  '&.³´*  r s  
 s
 t

 # @ÁbN[]\kjbhM # %²]" '&BBB&)²CCN ,  '&.³´*  r  s   &LoL s 
% t
%Ä
%Å # @À'b[\kjb M# %&BBBN&' & ,r
 & ,
r
Ä
%

 and
(Here @ may be in the list of 
, and VÆM , and each of  % t
and % is obtained from ht &LoL
by replacing all occurrences of @Áb[\kjbKM with @À'b[\kjb M.
Ordering of Actions: &LoL'& *È &LoL+À.bN[]\kjb M+À'b[\kjb M  #.
(where  is an action predicate of message M % with VXM % .)
CN;: Firstly Sends is used to derive a 1
predicate, and Ordering of Actions is used to derive an order ofÇY<[]\3[^7_a`5[cbo'&

actions performed by different principals. (This is essentially the same as AF3 presented in Table 5 of p.23 of [4].)For the same reason as the case of weakening rules and honesty inferences, we should restrict the application of¼L¼LFirstly Sends by the same condition.

6
Here we point out another way for keeping the weakening rule meaningful: introducing the logical negation and separating theÉ¿ÊlËÌ Ì
weakening rules into two rules as follows.

ÍJÎ Í ÅÏ }¿ÐxÑ".3Ò¸ ÉlÊËÓÍ3Ì ÎÍ Î Í ÌW(Act)   Ï-Ô Í ÌÍHere if   is } ’s sending of message Õ such that ¸×ÖWÕ , and  includes another } ’s sending of message  , then Ô isØ }Ð57Ñ'JÒ¸  , and if not, then Ô is }ÐxÑ"'3Ò¸  . This way is essentially the same as [3, 4]. (The Freshness Loss Axiom inTable 4 of p.22 in [4] is the corresponding axiom.)5

CCnoÓH K*  &.ÛC&)H
ÛC& &)H & H &)H &31 4
;{=Çb[\kjbÙRÓÚ
D
D T'#)=Ç^)[)ec[]f g[cbÙR Ú F O F D Ú¶PCÜQ®ß Ý<Þ TnÓH K*  &.ÛC&)H
ÛC& &)H & H &)H &134
D;{=Çb[\kjbÙRÓÚ
D]T'#)>ÆbN[]\kjbKMÈ#)=X^)[)ec[]f g[]bàR Ú F O F D ÚáP ÜQ ß Ý<Þ T±]r '& CCnoÓH q*  &.ÛC&)H&Óä&L & H &)H &% 134
D ÛC& &)H {=Ç
D T'#)>âbN[]\kjbÙRÓã
F O F D Ú¶P Q ß Ý Þ T'#& bH []\3&)jH bàRÓÚ&=X^)[)ec[]f g[]bàR Ú F O F D ÚáPCÜQ®ß Ý<Þ T±];r '&)±]r '& nÓH 0*   ä»p
& p
&L pÆH &L pdH= ã &.> ÛC&)H D
D FF±];r '&)±]r % '& 134 nÓH D 0*   % 13ÛC4 & &)H & D H &)
{

Z
=

b

[
k
\

j
å
b
Ó
R
Ú
c
D
'
T
#
H &
ÛC& &)H & H &)H &>dbN[]\kjbÙR Ú F O F D ÚáP Q ß Ý<Þ T'#)=Á^)[)ec[]f g[cbÙR Ú F O F D Ú¶P ÜQ ß Ý<Þ TZ ,  ±cro '&)Zcr; '&)Zcr  '& nÓH q*  &.Û&)H#
{>â^)[)ec[]f g[cbÙRÓÚD
D T'#
ÛC& &)H & %H 13&)4H &>dbN[]\kjbÙR Ú F O F D ÚáP Q ß Ý<Þ TnÓH K*  &.ÛC&)H
ÛC& &)H & H &)H &134
;%-{=ÂÀ'b[\kjbÙRÓÚ
D
D T'#)=Ç^)[)ec[]f g[]bàR Ú F O F D ÚáPCÜQ ß Ý<Þ T
Z ,   ±cro '&)Zcr; '&)Zcr  '& nÓH q*  &.ÛC&)H# &)H % {>æ ^L[.e'[f9g"[cbåRÓÚ
D T'#
 ÛC& &)H & % H 134 &)H & D> ÈÀ'b[\kjb R Ú F O F D Ú¶P Q ß Ý<Þ T F± ,  ±cro '&)Zcr; '&)Zcr  '& nÓH q*  &.ÛC&)H&.ÛC&)H± ,   # ±cro '&)Zcr; '&)Zcr  % '& 134 nÓH D q*    % {=À.bN[]\kjbàRÓ Ú ÛC& &)H D T'#)& >æH ^L[.e'&)H[f9g"[c& båRÓÚ
&)H D T 
%
%
#
3
1
4

{

ç
>
.
À
N
b
]
[
k
\

j
b
R
Ú
O
á
Ú
P
T
D
F
F
D
F #
Q®ß Ý<ÞÛC& &)H & H &)H &=X^)[)ec[]f g[]bàR Ú F O F D ÚáPCÜQ ß Ý<Þ T
Z ,   ±cro '&)Zcr; '&)Zcr  '& nÓH q*  &.ÛC&)H&.ÛC&)H#
 % {=À.bN[]\kjbàÛRÓÚ& &)H &D]T'#)H >æ&)^LH [.e'[& f9g"[cbåRÓÚ
DcT'#
ÛC& &)H & % H 13&)4 H & D>ÈÀ'b[\kjbåR Ú F O F D Ú¶P Q ß Ý<Þ T'#)=Á^L[.e'[]f g[]båR Ú F O F D Ú¶P ÜQ ß Ý Þ T± ,   ±cr  '& CCnoÓH K*  &.ÛC&)H&.ÛC&)H#% 134ÛC& &)H & D H &);H %-{=Â& À'b[\kjbÙRÓÚ
D T'#)>âÛ^)[)& ec[]&)f H g[]bà& RÓÚ H &)H D & T'#>èÀ.bN[]\kjbåR Ú F O F D Ú¶P Q ß Ý<Þ T'#)=Á^L[.e'[]f g[]båR Ú F O F D Ú¶PCÜQ ß Ý Þ T

PA(1),NV1(2),Hon(M)(3),Hon(S)(3),(4),Eq(4),Hon(R),Eq(1),FS(6),FS(7),(8),OA(5),(8),OA(8),(9),(10), ;Hon(W),Cont(11), ;,

(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)
(9)
(10)
(11)
(12)

Table 1: = ’s view at end of run following the initiator’s role of Challenge-Response Protocol

3.2 An example of correctness proof
Table 1 is the full proof of matching conversations of CR protocol from initiator &'©&L = &L’s viewpoint. A proof of thesame conclusion is presented in Table 10 of p.49 in [4]. CR protocol é 
D F  described in an informal
description is as follows.
1.
2.
3.

ë
 ê
ëê



êì

.
.
.

ä& &LR Ó& äã &L D T&  &L &ÓäRÓäã & &  F O &L F & D P Q í Ý<Þ T
R ã O D F ã P Q î Ý<Þ T

&.ÛC&)HIn this table, for readability we use some abbreviations as follows.  is a sequence =Çb[\kjbÙRÓÚ
Û& &)H & H &)H &&.ÛC& H &)H &.Û D]T'#=X^L[.e'[f9g"[cbÙR Ú F O F D Ú¶P ÜQ ß Ý Þ T'#k=Xb[]\3jbàRÓÚ
O D F P Q ï Ý<Þ T .  % is the sequence obtained from  by

 &.ÛC&)H &)H ± ,   Zcr Zcr  %and=& À.bN&L[] \kjb  RÓÚ D CT N D . Each symbols
D T with ä&Óäo&L &  &L , &Óä^)[)ec[]f g[]bàR ã D T ,b[\kjbÙRÓãandF O F D P Q íÝ Þ T
 &Óä&L &  &L &Óä&  &L &ÓäL
À'b[\kjb RÓã
F O F D P Q í Ý<Þ T O F D P Q í Ý<Þ , respectively. We also omit the predicates concerning information about keys: in this protocol, AÂµ and Að are the public keys for = and > , respectively, andAçµ ñ D and Aòð ñ D are the secret part of these keys, respectively. Moreover, some predicates not related to the derived
predicates at each line are omitted. (i.e., we implicitly use the contraction rules of non-commutative conjunction.)
H &)H &
Finally, M on Line (2) is a message such that O F
D Ú¶P Q ß Ý Þ VXM .
&.ÛC&)H

replacing the first action =XbN[]\kjbàRÓÚ
²]
are abbreviations ofFirst we would like to focus attention on the use of non-monotonic predicate fsends. On Line (6), the conclusion
is the agreement property from = ’s viewpoint. Note that we do not use fsends to prove the agreement property.
Therefore, if we want to prove the agreement property of this protocol, as we have also shown in our previous
paper [9], we do not need to introduce any non-monotonic predicate.

6

CN;: 
to derive the orderings between = ’s action and > ’s one. Particularly, the orderÛC& )& H & H &)H is used&
Û& &)H & H &)H &>ÈÀ.bN[]\kjbàR Ú F O F D ÚáP Q ß Ý<Þ T'#J=Á^L[.e'[f9g"[cbÙR Ú F O F D Ú¶P ÜQ ß Ý Þ T on Line (10) is derived by Firstly
The predicate 1

Sends and Ordering of Actions, and it cannot be derived without such non-monotonic notion. (The same property;:<
is derived on Line (10) in the example of [4] by means of the AF3 axiom.) In this proof, 1
is introduced on
Line (7) by using the cut rule and the weakening  rule for actions as follows: first, by applying the cut rule to (1)nÓH 0*&.Û&)H
ÛC& &BBB
{=XbN[]\kjbÙRÓÚ
T , and then by applying
and FSends we obtain the sequent 134
D
D T'#)=Á^L[.e'[]f g[]bàR Ú
some weakening rules for actions we obtain (7). Here we point out that at the second step each application of the¼L¼LH
condition that “no predicate of the form =XbN[]\kjbhM (with D¿VdM ) does not
weakening rule is restricted by &.ÛC&)H &)H 
appear before =EÀ'b[\kjb RÓÚ
D T D in the action operator (i.e., in the square bracket [ ])”. However, in thiscase, we can obtain the sequent (7) by any order of applications of weakening rules for the components of thissequence. (Line (8) is similar to (7).)
By introducing the non-monotonic predicate, all weakening inferences for concrete actions and for honesty
¼L¼L
assumptions below the application of Firstly Sends on Line (7) and (8) are restricted byconditions that “= ’s&.ÛC&)H
ÛC& &)H & H &)H &sending of RÓÚ
D T (introduced at Line (7)) and > ’s sending of R Ú F O F D ÚáP Q ß Ý<Þ T (introduced at Line(8)) cannot be inserted before the corresponding actions”. The information about orderings are necessary forproving our aimed property. Therefore, if we want to prove a weaker property such as the agreement property, as
we have shown in our previous paper [9], we don’t have to introduce such non-monotonic predicates. Note thatin our system we do not use any temporal operators for deriving properties about the orders of principals’ actions:our formalization only use the non-commutative conjunction.
Remark. In our proof, Line (3) is derived by honesty inference Hon(Match). The intended meaning of thisH &)H &
ÛC& &)H & H &)H &inference is “if > sends a message including O F
D Ú¶P Q®ß Ý Þ , then > should send R Ú F O F D Ú¶P Q®ß Ý<Þ Tr
under the assumption that > honestly follows ”. we restrict applications of the weakening rules to satisfy the
¼LH &)H &
condition that “ ’s sending action of a message including O F
D Ú¶P Q ß Ý<Þ does not appear in the honesty
assumptions”. Here we point out that we formalize this kind of inference by some restrictions instead of using
logical negation. On the other hand, in the proof in [4], the same conclusion is derived by the honesty assumptionHÛC& &)H & H &)H &that “if > does not freshly generate F as a fresh value, then > should send R Ú
F O F D ÚáP Q ß Ý<Þ T under thenassumption > is honest”. This implication is obtained by using óh¾¿4.

4 Trace Semantics and Soundness of the System
In this section we give a semantics for our inference system. First we give a definition of the semantics (in Section4.1), and next we give a sketch of soundness proof of our system (in Section 4.2).

4.1 Trace Semantics
Our semantics is based on the notion of trace, which is a sequence of states. A state is a multiset of primitive states '&'ô '&BBB
M
of the form “principal  has information M ”, and denoted by  M. We also introduce a special kind
H+ & of primitive state “message M sent by  is currently transmitted through the network”, and denoted byM  .
The notion of state is defined by the same way in Multiset Rewriting System [2], however we use it as semantic
notion.
Uõ&. &BBB
For preparing the definition of the semantics, here we introduce some notions and notations.
areD& &BBB
used to denote states and ö ö %to denote sequences of states, namely traces. We also introduce some notions

related to traces. The notions of membership relation (denoted by ¡ ¢Ãö ), order relation on ö (denoted by ¨¿÷ ),and extension (denoted by ö°´ö"% ) are defined by the same ways as those of sequences of actions. (See Section2.1.) When ¡ is the 2 -th element of ö , the number 2 is called the position of ¡ in ö . We denote the number of
 


 p
 '&  '&'ô pºüO M  M
M P , then ø ¡Õø ·ûú
occurrence of facts  M
in a state ¡ by ø ¡Õø · ú (e.g. if ¡
).

t!ù

t!ù

7

N8J .&   ¡ &isBBused
B& to denote the set of key possessed by principal&BBBN&  at position ¡ . For messages M , M % and a set
IaýP , “M is accessible in M % with keys OCI DIaýP ” (denoted&byof keys OCI D
BBBCM§& ¢!þxÿ Þ  ÿ0M % ) pis the¦&BreflexiveBB&L
transitive closure satisfying the following conditions: (i) M ¡ ¢ þxÿ Þ  ÿ   R M+D, (ii)M S T for some 2
p ¦&BBBC&)6
MW¢oþxÿ Þ  ÿ  ÙONM+P ÿ for some ¥.
A

In this section, we assume that all states except for states of network are monotonously increasing for any trace.
That is, we consider only traces where, once an information is possessed by a principal, it does not disappear in
his/her memory.
By means of the notion of traces, truth conditions for predicates of our syntax is defined as follows. We denotep
the basic semantic relation “  is true at state ¡ in ö ” by “ ÷ ¡   ”.
Truth condition for predicates:¬ p  B{       '& 8 &  
 I % AlÚ254 I I % ¢ ¡ and
I % ¢ ¡ .
¬p  &' B{       '&'ô  
iff  II  ¢   ¡  and
I ¢ ¡ .
    pÆiff¡     ¡ % H+ .  &   
H+ &  ¡¡
iff  M
,
and
¢
D
M

¢
D
 BÓH²N] ñ &  H²ñ N] &    M    ¢ ¡ .
MM¢ ¡ andiff ¦åp ¢ ¡  ñ D andø ¡ ñ¤ D ø t!ù ·ûø ¡$ø t!ù ·ûú , andú 
ONM  P ÿ ¢ Q  ! ù t ¦®
ú M  and
" # pp ¦&BBBC&Lø ¡ ñ D  ø t!ù · ø ¡0ø t!ù · ú for each ¥
.
ú

p
  
  
iff  M¢ ¡ D and  M  ¢  o ¡ . 
 B{   o ñ  p ÷ ¡  XY [\3n[] ^L_"`5 []bhMM¢ ¡ ñ D and ¢ ¡ ) and VXM .
iff 
÷
¡
 134
p
 &Lopiff÷ ¡  ²À'b[]\3jb M¬ ÷ ¡  i
B ¬ b[]\3jb!M B{and p ¤ VXM and ¥ $Z2 M % & M
÷ p  =ZbN[]\kjb!M % .
pp%iff÷ ¡   D #£££N#.S÷ ¡ Þ   D and £££ and÷ ¡   ;S ,and 2LD ¨ £££ ¨ 2 S»¨ ¡ .
pNext, the definition “  is true for trace ö ” (denoted by ÷à ) is as follows.
¬ p ,B{ p , 
0
÷
¡
iff
, or +¢ö} *©L }-Ò ,  or 
} /1.
 (  .)pn  ÷ ¡  B{ p (where ')CC(Eno +MM .
iff  ¡h¢Èöp ÷ 134B{ p ÷ ¡  134(where each Í # is an action predicate.)÷  D #£££#.S iff  ¡o¢Èö÷ ¡   D #£££C#.;S
p (
p 
p ,
p
p ¦&BBBC&L
(+p  &BBBC& ,  & &BBBC&S ).
” (where
We define that ÷ iff “ ÷  and . . . and ÷ , and ÷ ¡ for each 2
aD p;:<
By the above definition, it is clear that for any  except for 1(i.e., for the case that  is monotonic), if ÷àpthen ÷   for any ö©°Æö % .
In terms of the above definitions, we define that the basic form of assertion is true under ö , namely, ²] '&BBB'²]  ²]  '&BBB&)( p  ÷   t D #£££#
 St
 D #£££#
 ÿ
-

p

 & 
÷ ¡  lA  I
p
mÿ 
÷
¡
 
p
qpi


% (for any terms and % )p ÷ ¡ p ÷ ¡  Ãb[\kjbKM&BBB&ONMESkPCÿÜ ÷ ¡  i^)[)e'[f9g"[cbKM ONM D PCÿÜ Þiffholds if and only if the following is satisfied (where  is a state predicate or a sequence of action predicates).

¬

KB ¬

B{ p

2%2$X2÷  ¡tIf C1 2 ¨¬
B{
KB{ pC2 3ö % ö©°âö %54 2 ¨
p (C3 ÷ ,p 
C4 ÷  ,pthen ÷à .

­ p

­ p
¬

B¬
B{ p

÷  ¡t  , and ¥ ¨ I ¥a%3$è¥û÷û ¤ ÷û ¤   ,
¤ L
 ¬
B{ p
÷  ¡ 4 ¥ ¨ I÷  ,²]

²CCN&

Here for each honest predicate
76¡ , if it is of the form
86¡ M9¡6 for¦&BBB&L
¦&BBB&
I (i.e., M 6¡ is not empty), then the following condition is also satisfied:
or
8



p


&'

and for 2

p

¬

M %

B{L

M %2& M96¡



4



M %

p

M %%



4



:6¡

p

 ­

¬

L
b[\kjbhM % .
CN&
The reason why we need this additional condition is as follows: first recall that<6¡ M96¡ (where M=6¡
bN[]\kjbhMÂ% % ) and he/she does
is not empty term) means that “ honestly follows the sending action  6¡ (say,not follow any other sending actions of the message M % including =M
6¡ ”. Therefore, to satisfy this restriction, weassume b[\kjbKMÂ% % is false for any extension ö"% of ö .
If the above form of assertion is true for any trace ö , then this assertion is called valid and we omit the subscription ö .
C5b[\kjbhM % %ö %;& öB{ p÷Remind that in this paper we consider only protocols which do not include any duplication of primitive actions.
We assume that all traces considered here are also restricted by the same condition. (Formally, for any state ö and
p>
p? ¤
p
for any action predicate  , if
÷ ¡   and ÷   then 2 ¥ .)4.2 Soundness of the System
In this subsection we show a sketch of a soundness proof of our system. In our previous paper [9], we presented asoundness proof for the system including only monotonic predicates. Then, here we only consider some of cases;: .
related to the non-monotonic predicate 1
D CF , and ¸lÖ
(where L Þ   ÖA B , and )o 'Þ &  EÖ
 &'L'&
 &LoL'&  @)ÒC Þ ÒHG'ÒAF .) A *ÈA çÀ. bN[]\k&Ljob L M F 
ÇY<[]\3[^7 _"`5[]b L d ^L[.e'[]f g[]b!M=I  ²À.bN[]\kjb M F#^L[.e'[]f g[]b!M=J ONM D P ÜQ #bN[]\kjbKM9K # d^)[)e'[f9g"[cbhM=I

Nonce verification 2:p &BBBN&.

Assume that all the predicates appearing in the left hand side are valid. That is, for any ö (S ), (i)D¬KB ¬ p   BL
D  ¢  ¤  4    A ñ D  ¢   ¤ L , (ii)   ¡ B{L p ÷ ¡  ÁbN[]\kjb!M F  4  ¬ ¥a%M$º2 D B{ p ÷ ¤ 
¥L$
A
ñ

Þ

LL
B{ p
oÞ 
B{ p
ÁbN[]\kjb!M % with  VëM %  , (iii) <2 F $ 2 D÷ ¡ @  Z Y<[]\3p  [^7_a`5B [cb , (iv)B{ <p?2 JON 2 D ÷ ¡ B  i ^)[)e'[f9g"[cbhM=I with(iii) and (iv), V p  M I B, ONM+DP Q B{LV×b[6xB{\kLj bKM I 6 holds, and p then÷ ¡G 
 M  oI  . From  (ii), ¬UTVp  & B{ T  o  LL  U2 K $ 2 J4 <2RI>$æ
2 D $ $Æ2RI 4
÷ ý
QP
 2SK P LL ¢ I 6 B{LÓ6
6  P  p ¢È2RI . Then by (i) and (ii), %
4and  %
^L[.e' []f g[]b!M=J ONM D  P ÜQ
$

b

[
k
\

j
K
b
=I withM
V
9K . This is the truth conditionMý÷L 
^L[.e'[]f g[]b!MWJ ONM D PCÜQ #b[]\3jbKM9K , and therefore, the sequence of actions in the right hand side of theforsequent is true.
Firstly Sends:(Without loss of generality, here we only consider a special case such that only  ’s honesty assumptions appear
in the left hand side of each sequent and omit any context for readability.)
BBB
q*  r  s   s t D # #. St
 # ibN[]\kjb!M # %²]
BBB
q*  r  s   &LoL s 


%
#
.
#


%

#
+

.
À
N
b
]
[
k
\

j
b
M
t
t
S
D

p
 # % &Lopp(Here VXM , and for each  ¡% t ,  ¡% tif o¡t²À.bN[]\kjb M
ib[\kjbhM , otherwise  ¡% t¡t .)p
(i.e., !t does not contain ÁbN[]\kjbhM ).
Here it is clear that the soundness holds when  ¡% to¡t p for all 2>$p &LoÃb[\kjbhM and ¡% t
²À'b[]\3jb M
Then, from now we shall consider only thecase that  ¡t
for some¼L¼L ss¤ p, does not include
2 $ . (In this case, by the conditionXÃb[]\3jbKM % with VXM % for all ¥%$Ç2 .)First, consider a trace ö satisfying the conditions C1 and C2 (previously shown in the definition of truth con
;: dition for the sequent) for, ö also
 % D t ²#£££C#. ]S% t . By the definition of the truth condition for 1


#

£

£

£
.
#

satisfies theconditions
C1
and
C2
for
”.
Here
we
assume
that
the
upper
sequent
isvalid,
t
t
S
D
p s
s
CN%then ÷ #)Ãb[\kjbKMÈ# % holds. Moreover, if we assume that ö satisfies C1 and C2 for

t

#

£

£
C
£
.
#
¬
p
p
 &LoL
B{ p D
  %S t ,then by C1, the following holds that “if ÷  %¡, then Y
²À'b[\kjb M %¥ $Á2ÁbN[]\kjbhM % with VÁM %
¬
p
B 
p ¤
M
¥
$Æ2
â
V
Â
M
%
%
and MÂ%”. Therefore, Z. This is the truth condition for÷ ÃbN[]\kjbKME% % for any ME% % with M
p s÷ #)ÃbN[]\kjbKM . Therefore the right hand side of the lower sequent is valid.

Weakening rules:
9( &)²CCN  K*  , q
ot$#  % t(q&)²]" q*  ,  W(Hon)
ot #. % % tû#  % t


(²*   $# t % t  W(Act)(+*  t #. % % tû#  % t! 


&Lo

(Here we only consider the case that  % % t is ib[\kjbhM . It is similar way to prove the case that  % % t is ²À'b[]\3jb M(1) Weakening (Honesty):
¼L¼L
Here we assume that the lower sequent satisfies thecondition. That is, 0% t does not include any action of &Lo
the form +À.bN[]\kjb M %with VXM % . It is sufficient to show that for any trace ö , “if ö satisfies the conditions C1²CCN CN   t #.% % t # % t , then ö also satisfies the conditionC1
 t #  t ”, howeverand C2 for;:<and C2 for¼L¼L
it immediately follows from the definition of the truth condition of 1
and thecondition.
(2) Weakening (Actions):
¼L¼L
 &Lo&Bycondition, we can assume that h% t does not include ²À'b[]\3jb M%with VÆM ME% . It is sufficient
p  
 
p  
to show that for any trace ö , ÷ ot # ib[\kjbhM #  % t then ÷ ot #  % t , however, this immediately follows from
p  
 
the definition of ÷  t # ib[\kjbhM # ;% t .

¼L¼L

condition (i.e.,Remark. As for the weakening rule for honesty assumptions, if the lower sequent violate the &Lo
if  % t includes action predicate of the form ²À'b[]\3jb M %with VâM % ), then there exists a trace such that it²]" ²]"   t #.;% % t # % t whereas it satisfies
 t # ;% t . The same is true
does not satisfy the conditions forof the other weakening rule.

5 Conclusions and future work
By the distinction between monotonic and non-monotonic predicates, we gave the way to include non-monotonic
properties, and showed that they can be used in more powerful derivation to prove correctness properties of a
protocol. As an example, we proved the matching conversations of CR protocol, where the ordering of actions
performed by different principals are derived by Firstly Sends and Ordering of Actions. Other examples are
Nonce Verification 2 and 3 presented in (II-2) of Appendix. These are formalizations of the notion of Outgoingtest in the Authentication tests based Strand space method (cf. Guttman-Fábrega [7]). This notion can be forCN;: malized only by using non-monotonic property 1
or similar one, which can represent the same notion ofuniquely originates (in [7]).
In our extended system, we did not use logical negation, nested implications and any temporal operators toprove our aimed property, which were used in [3, 4]. (In other words, in our system each sequent is the form ofHorn-clause.) This simplification is realized by the restriction on the honesty inferences. However, this restriction
is a trade-off. For example, the following kind of inferences cannot be expressed in our system: assume that a pof a protocol. Then from this assumption, we canprincipal (say  ) is honest following a role , ©   , D #.p  F #.87J [Z²]  , p+[Z , pconclude that “ 4  performs
:J ” (i.e., “if  is honest and

D
F
,
6Åä3n
he/she performs an primitive action then it is ûD or Ú
Ú<F or  J ”), because honest principal does not perform
any other actions than the actions defined by his/her role. One of our next aims is to investigate the formalizationof such inferences and clarify what kinds of properties (useful for a correctness proof) become provable in suchextended system.
We also gave a semantics based on the notion of trace and show a sketch of soundness proof. This direction
should make a contribution to our further target, namely, automated generation of correctness proofs or correct
protocols for example.

Acknowledgments
We would like to express our sincere thanks to Drs. Andre Scedrov and Iliano Cervesato for their invaluablecomments and discussions. We also would like to express our sincere thanks to Mr. Lam Ta-Minh for his helpful
10.)comments. Finally, helpful comments from the anonymous reviewers results in improvements to this paper.

References[1] M. Burrows, M. Abadi and R. Needham. A Logic of Authentication. Technical Report 39, Digital System
Research Center, 1989.
[2] I. Cervesato, N.A. Durgin, P.D. Lincoln, J.C. Mitchell and A. Scedrov. Multiset rewriting and the complexityof bounded security protocols. Journal of Computer Security, vol.12, no.1, pp.677-622, 2004.
[3] A. Datta, A. Derek, J. C. Mitchell and D. Pavlovic. Secure Protocol Composition. Proceedings of 19th Annual
Conference on Mathematical Foundations of Programming Semantics, ENTCS Vol. 83, 2004.
[4] A. Datta, A. Derek, J. C. Mitchell and D. Pavlovic. A Derivation System for Security Protocols and its Logical
Formalization. Journal of Computer Security, Special Issue of Selected Papers from CSFW-16, 2004.
[5] W. Diffie, P. C. van Oorschot and M. J. Wiener. Authentication and authenticated key exchange Designs,
Codes and Cryptography, vol.2, pp.107-125, 1992.
[6] N. Durgin, J. Mitchell and D. Pavlovic. A Compositional Logic for Protocol Correctness. Journal of Computer Security (Special Issue of Selected Papers from CSFW-14), 11(4), pp.677-721, 2003.
[7] J. D. Guttman and F. J. T. Fábrega. Authentication tests and the structure of bundles. Theoretical Computer
Science, vol. 283(2), pp.333-380, 2002.
[8] K. Hasebe and M. Okada. A Logical Verification Method for Security Protocols Based on Linear Logic and
BAN Logic. M. Okada, B. Pierce, A. Scedrov, H. Tokuda and A. Yonezawa (eds.), Software Security —Theories and Systems, Lecture Notes in Computer Science, Hot Topics, vol.2609, Springer-Verlag, pp.417440, 2003.
[9] K. Hasebe and M. Okada. Inferences on Honesty in Compositional Logic for Security Analysis. to appear inProceedings of the International Symposium on Software Security (ISSS2003), Springer LNCS, 2004.
[10] T. Y. C. Woo and S. S. Lam. Verifying authentication protocols: Methodology and example. Proceedings ofthe International Conference on Network Protocols, 1993.

Appendix: axioms and inference rules of the system(I) Logical inference rules(1) Structural rules: weakening, contraction and exchange rules in the left hand side, and cut rule (Cut) (2)Inference rules for equality (Eq) (a typical rule which we often use is presented below), (3) Substitution rule
(Subst), (4) Inference rules for non-commutative conjunction (;): Concatenation, Weakening and Contraction.

(²*  &.³ *  (²*   Âpi ³º*    
(  *      %       ] Subst
Eq(0&.³´*  (0&.³´*    (  ] *    
Cut
 \
 

 
 

,  ,  &)(È*  (²*   ,  ,³º*   , , (²*   ,  , , 
 # % %
 % %% # %
# %
 
 # % % # %Weak-;
Concat-;Cont-;,  , ,  &)(È*  (0&.³´*    ,  , , (È*   ,  , $# %Å # % %Ó# %# %% %
; 
 # %

(II-1) Axioms about primitive actions* 

 D #£££N#.S 9 D #£££N#.S
11

(II-2) Axioms for relationships between properties(Here axioms including non-monotonic property are marked by ¹ .)Freshness 1:

XY<[]\3[^7_"`5[]b

 *

134

CCno oK* (where
CCino Ö   .)
M
134
M %

Freshness 2:

n

134

:
`
^
_
Nonce Verification 1:ÖG  ÒÓ    .)
 &'L'& CCno (whereL'& Ll
Lq*È
 

L
A A
134
M
æ^)[)ec[]f g[cbhM % ONM+P ÜQ Ý Þ
bN[]\kjbhM % % # d^L[.e'[f9g"[cbhM % NO M+P ÜQ Ý<ÞD CF and ¸ÖG(where L Þ   ÖA B and Lo '&Þ   EÖ
 &'L'&
 &LoL'&  @'ÒÓC Þ ÒÓCG'ÒCF .) A *ÈA çÀ. bN[]\k&Ljob L M F 
ÇY<[]\3[^7 _"`5[]b L d ^L[.e'[]f g[]b!M=I  ²À.bN[]\kjb M F#^L[.e'[]f g[]b!M=J ONM D P ÜQ #bN[]\kjbKM9K # d^)[)e'[f9g"[cbhM=I

Nonce verification 2 a :D  F is also satisfied.)(additionally to the condition for Nonce Verification 2, L Þ   Ö&'L'&
 &LoL'&
o'&
'&
'&
 & LA * AÇY<[]\3[^7_"`5[]bd^L[.e'[]f g[]b!M=I
bN[]\kjb ONM9KP %Q
lA A % =p çÀ.bN[]\kjb M F
M=I ON9
M KPN%Q
 &'
m Q  , respectively.
We also admit axioms obtained from Nonce verification 1-3 by replacing lA A
with 
Shared secret: (where *  Ö Þ Ò @ .)

'&
'&
'& Q '& Qm @ K*È mQ  ibN[]\kjb$ONM+DP Q Þ db[\kjb ONMÂFP Q @ ÃY []\J[]^L_"`5[cbKA %  m Þ@@Nonce verification 3 a :Firstly Sends a :This rule satisfies cb-b  condition (cf. Section
 3.1).

²CCN '&BBBC&)  , '&.³´*  r s  
 s

ot
 # @ÁbN[]\kjbhM # %²]" '&BBB&)²CCN ,  '&.³´*  r  s   &LoL  s 
% t
%Ä
%Å # @À'b[\kjb M# %ÇY<[]\3[^7_a`5[cbo'&

(where Í is an action predicate of message  &LoL'& * &Lo  with ¸lÖ  .)+À.bN[]\kjb M²À'b[]\3jb M#.Ordering of Actions a :(III) Honesty inferences

For (1) Substitution and for (3) Deriving another action, we also admit the inference rules obtained by replacing “ucvLwxv)yzNv.| ” with“dvL¸ vLuev.| ” or “ |LvL¸a| ”, respectively. These rules satisfy the cb  (cf. Section 2.2 (III)) and cb-b  conditions.

(1) Substitution: ] ( *   ² )^ [)ec[]f g[]b!M(0&) CN
q*   Epi H(S)^L[.e'[f9g"[cbhM(where iÖl .)(+*   ,  
 r
 #
bN[]\kjbKM #(q&)²]
& K*   ,   r  H(M)bN[]\kjbhM % M
 # bN[]\kjbKM % #(2) Matching:(3) Deriving another action in a role:(²*   ,   r  # b[\kjbhM #(0&) CN K*   ,    r  H(R)
%
%
L
^
.
[
'
e

[
9
f
"
g
c
[
h
b
M
#
N
b
]
[
k
\

j
K
b
M



#
L
^
.
[
'
e
]
[
f

g
]
[
!
b
M
#
b
N
]
[
k
\

j
K
b
M
#


(IV) Weakening rules for actions and honesty assumptions

Weakening rule for honesty assumptions (left below) satisfies cb  and cb-b  conditions, and weakening rule for actions (right below) satisfies

cb-b  condition.
(q&)²]"  K*  , 
ot #  % t(0&) CN
 K*  ,  W(Hon) t #.% % t # % t

(+*   tû#  % to W(Act)(²*   t #.;% % t # % t  12