Model-based verification of a security protocol for conditional acess to services
(1999) Formal Methods in System Design : an international journal — Vol. 14, n° 2, p. 171-191 (1999)
Files
RUN-PP99-01.pdf
Restricted Access - Adobe PDF
- 391.99 KB
Details
- Authors
- Abstract
- We use the formal language LOTOS to specify and verify the robustness of the Equicrypt protocol under design in the European OKAPI project for conditional access to multimedia services. We state some desired security properties and formalize them. We describe a generic intruder process and its modelling, and show that some properties are falsified in the presence of this intruder. The diagnostic sequences can be used almost directly to exhibit the scenarios of possible attacks on the protocol. Finally, we propose an improvement of the protocol which satisfies our properties.
- Affiliations
Citations
Leduc, G., Bonaventure, O., Leonard, L., Koerner, E., & Pecheur, C. (1999). Model-based verification of a security protocol for conditional acess to services. Formal Methods in System Design : an international journal, 14(2), 171-191. https://doi.org/10.1023/A:1008683519655 (Original work published 1999)