A real-time process algebra, enhanced with specific constructs for handling cryptographic primitives, is proposed to model
cryptographic protocols in a simple way.We show that some security properties, such as authentication and secrecy, can be
re-formulated in this timed setting. Moreover, we show that they can be seen as suitable instances of a general information
flow-like scheme, called tGN DC, parametric w.r.t. the observational semantics of interest.We show that, when considering timed trace semantics, there exists
a most powerful hostile environment (or enemy) that can try to compromise the protocol. Moreover, we hint some compositionality
results.
Work partially supported by MURST Progetto “Metodi Formali per la Sicurezza” (MEFISTO); IST-FET project “Design Environments
for Global ApplicationS (DEGAS)”; Microsoft Research Europe; by CNR project “Tecniche e Strumenti Software per l’analisi della
sicurezza delle comunicazioni in applicazioni telematiche di interesse economico e sociale” and by a CSP grant for the project
“SeTAPS II”.