Sciweavers

POPL
2005
ACM
13 years 10 months ago
Specifying Kerberos 5 cross-realm authentication
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,...
POPL
2005
ACM
14 years 4 months ago
Statically checking confidentiality via dynamic labels
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...
Bart Jacobs, Wolter Pieters, Martijn Warnier
POPL
2005
ACM
14 years 4 months ago
Inferring authentication tags
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...
POPL
2005
ACM
14 years 4 months ago
Policy framings for access control
Massimo Bartoletti, Pierpaolo Degano, Gian Luigi F...
POPL
2005
ACM
14 years 4 months ago
Formal prototyping in early stages of protocol design
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...
Alwyn Goodloe, Carl A. Gunter, Mark-Oliver Stehr
POPL
2005
ACM
14 years 4 months ago
Enterprise privacy promises and enforcement
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...
Adam Barth, John C. Mitchell
POPL
2005
ACM
14 years 4 months ago
A bisimulation for type abstraction and recursion
traction and Recursion Eijiro Sumii Benjamin C. Pierce University of Pennsylvania
Eijiro Sumii, Benjamin C. Pierce
POPL
2005
ACM
14 years 4 months ago
Mutatis mutandis: safe and predictable dynamic software updating
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,...
POPL
2005
ACM
14 years 4 months ago
A semantics for procedure local heaps and its abstractions
Jörg Bauer, Noam Rinetzky, Reinhard Wilhelm, ...