Symbolic Partial Model Checking for Security Analysis - Computer Network Security - page 122

Symbolic Partial Model Checking
for Security Analysis

Fabio Martinelli

Istituto di Informatica e Telematica - C.N.R.
Area della ricerca di Pisa, Via G. Moruzzi 1, Pisa, Italy
[e-mail]
Phone: [phone]; Fax: [phone]

Abstract. In this paper, we present a symbolic version of the Hennessy-
Milner logic for expressing security properties. The models of the logic
are CryptoCCS processes with their symbolic semantics. We study the
model checking problem and partial model checking techniques for the
logic.

1 Introduction

One of the main problems in the analysis cryptographic protocols is the uncer-
tainty about the possible enemies or malicious users that may try to interfere
with the normal execution of a protocol. The verification problem for a security
property may be naturally expressed as a verification problem for open systems
as advocated in [9,10,11]. Indeed, for every possible enemy X we have that

S | X | = F (1)

where S is a process in a concurrent language with as parallel composition

operator, as CCS (e.g., [13]), F is a temporal logic formula and

|

= is the truth
relation between processes and formulas. Roughly, if we imagine that F speci-
fies that the system under investigation is secure, then the previous statement
requires that the system S in “composition” with whatever intruder X is still
secure.
The universal quantification makes it dicult to deal with such verification
problems. A verification approach based on partial model checking and satisfi-
ability procedures for temporal logic has been proposed in [9,10,11]. Basically,
partial model checking is a technique which enables us to project the property
that a compound system must enjoy in a property that one of the components
has to satisfy. More formally, we can find a formula F// S

|

s.t.

= F// S
Work partially supported by Microsoft Research Europe (Cambridge); by MIUR
project “MEFISTO”; by MIUR project “ Tecniche e strumenti software per l'analisi
della sicurezza delle comunicazioni in applicazioni telematiche di interesse economico
e sociale”; by CNR project “Strumenti, ambienti ed applicazioni innovative per la
societa dell'informazione” and finally by CSP with the project “SeTAPS”.

S | X | = F iff X |