Information Technology Reference
In-Depth Information
Table 6.
Partial evaluation function for ( )
\ L
.
=
T
T
//
\L
.
=
K
A
K
A
//
\L
.
=
¬
(
F//
L
)
(
¬F
)
//
\L
M
:
α
(
F//
\L
)
α
=
c
!
m
and
c∈ L
M
:
α
(
F//
\L
)
α
=
c
?
x
and
c∈ L
M
:
α
(
F//
\L
)
α
=
τ
F
.
=
(
M
:
αF
)
//
\L
otherwise
.
=
∨
i∈I
(
F
i
//
\L
)
∨
i∈I
F
i
//
\L
5 Concluding Remarks
In [9,11], the use of contexts (open systems) has been advocated to represent
the security analysis scenario, where the holes denotes the components of the
systems whose behavior we are not able to predict. Then, the usage of partial
model checking to check such systems has been suggested.
Partial model checking is a powerful technique. It has been introduced to
perform ecient model checking; it has been exploited to perform the analy-
sis of security protocols; recently, it has been advocated for the compositional
verification of parametrized systems in [1]. So, we plan to extend these current
symbolic techniques on partial model checking for security analysis for such an
interesting scenario with unbounded processes.
In this paper, we set up a preliminary framework for symbolic partial model
checking of cryptographic protocols using almost generic inference systems. We
are currently working on optimizations and implementation details. In partic-
ular, we plan to extend the PaMoChSA tool (Partial Model Checking Security
Analyzer) [12] with such symbolic analysis techniques and then check the anal-
ysis differences between the two versions of the tool on the same examples.
Acknowledgments
We would like to thank the anonymous referees for their helpful comments.
References
1. Basu, S. and Ramakrishnan, C.: Compositional analysis for verification of param-
eterized systems. In
TACAS 2003
, vol. 2619 of
LNCS
2. Hennessy, M. and Milner, R.: Algebraic laws for nondeterminism and concurrency.
Journal of the ACM
(1985)
3. Ingolfsdottir, A. and Lin, H.: A symbolic approach to value-passing processes. In
J. Bergstra, A. Ponse, and S. Smolka, editors,
Handbook of Process Algebra
. North-
Holland (2001) 427-478
