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 tGNDC, 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 present some compositional proof rules for checking some non-interference security properties. We show an application of these rules to the analysis of a stream signature protocols, e.g. the Gennaro_Rohatgi and muTESLA.
Key words: Formal verification, cryptographic protocols, stream signature protocols.
| Fabio Martinelli |
| Visiting Fellow, DCS, ANU |
| Date: | Fri Aug 6 2004 |
| Time: | 1 to 2pm |
| Location: | Level 1 Seminar Room, CSE Bldg (K17), UNSW |
Last updated by rhuuck at Fri Aug 6 12:51:36 2004 GMT+1000