Cross-realm authentication is a useful and interesting component of Kerberos aimed at enabling secure access to services astride organizational boundaries. We present a formalizat...
Iliano Cervesato, Aaron D. Jaggard, Andre Scedrov,...
This paper presents a new approach for verifying confidenfor programs, based on abstract interpretation. The framework is formally developed and proved correct in the theorem prov...
We present PEAR (Protocol Extendable AnalyzeR), a tool automating the two static analyses for authentication protocols presented in [7, 8]. These analyses are based on a tagging s...
Riccardo Focardi, Matteo Maffei, Francesco Placell...
Network protocol design is usually an informal process where debugging is based on successive iterations of a prototype implementation. The feedback provided by a prototype can be...
Several formal languages have been proposed to encode privacy policies, ranging from the Platform for Privacy Preferences (P3P), intended for communicating privacy policies to con...
Dynamic software updates can be used to fix bugs or add features to a running program without downtime. Essential for some applications and convenient for others, low-level dynami...
Gareth Stoyle, Michael W. Hicks, Gavin M. Bierman,...