CiteULike: michaelbanks's Mantel:H [11 articles]

A unifying approach to the security of distributed and multi-threaded programs

Journal of Computer Security, Vol. 11, No. 4. (1 January 2003), pp. 615-676.

posted to translation security program maks language information-flow distributed 2003 by michaelbanks on 2009-10-30 14:16:44 as

Exploiting Generic Aspects of Security Models in Formal Developments

Mechanizing Mathematical Reasoning In Mechanizing Mathematical Reasoning, Vol. 2605 (2005), pp. 452-475.

by Heiko Mantel, Axel Schairer

posted to security maks information-flow formal-methods 2005 by michaelbanks on 2009-10-19 19:18:02 as

Automating proofs of unwinding conditions

In Proceedings of the Verify'06 Verification Workshop (2006)

by Dieter Hutter

edited by Serge Autexier, Heiko Mantel

posted to verification unwinding theorem-proving proof multi-agent maks information-flow automatic 2006 by michaelbanks on 2009-08-26 13:06:14 as

Security of multi-agent systems: A case study on comparison shopping

Journal of Applied Logic, Vol. 5, No. 2. (June 2007), pp. 303-332.

by Dieter Hutter, Heiko Mantel, Ina Schaefer, Axel Schairer

posted to security multi-agent case-study 2007 by michaelbanks on 2009-08-26 12:21:12 as

Combining Different Proof Techniques for Verifying Information Flow Security

Logic-Based Program Synthesis and Transformation In Logic-Based Program Synthesis and Transformation, Vol. 4407 (2007), pp. 94-110.

by Heiko Mantel, Henning Sudbrock, Tina Kraußer

posted to 2006 composition information-flow program proof security verification by michaelbanks on 2009-07-09 13:00:49 as

The framework of selective interleaving functions and the modular assembly kit

In FMSE '05: Proceedings of the 2005 ACM workshop on Formal methods in security engineering (2005), pp. 53-62.

by Heiko Mantel

posted to 2005 comparison information-flow maks property security selective-interleaving by michaelbanks on 2009-07-09 12:21:56 as

On the Composition of Secure Systems

Proceedings of the 2002 IEEE Symposium on Security and Privacy In Proceedings of the 2002 IEEE Symposium on Security and Privacy (2002), pp. 88-101.

by Heiko Mantel

posted to 2002 composition property security system by michaelbanks on 2008-11-25 16:06:36 as

along with 1 person jfischer

Possibilistic Definitions of Security --- an Assembly Kit

13th IEEE Computer Security Foundations Workshop (CSFW '00) In 13th IEEE Computer Security Foundations Workshop (CSFW '00) (2000), pp. 185-199.

by Heiko Mantel

posted to separability security possibilistic noninterference maks information-flow framework 2000 by michaelbanks on 2008-11-19 10:14:41 as

Unwinding Possibilistic Security Properties

Computer Security - ESORICS 2000 In Computer Security -- ESORICS 2000, Vol. 1895 (2000), pp. 238-254.

by Heiko Mantel

posted to 2000 nondeterministic noninterference possibilistic property refinement security theorem unwinding generalised by michaelbanks on 2008-11-01 18:46:39 as

A Uniform Framework for the Formal Specification and Verification of Information Flow Security

(July 2003)

by Heiko Mantel

posted to verification specification security maks information-flow framework formal 2003 by michaelbanks on 2008-10-29 17:50:22 as

Preserving Information Flow Properties under Refinement

In Proceedings of the 2001 IEEE Symposium on Security and Privacy (2001), pp. 78-91.

by Heiko Mantel

posted to specification security refinement property preserving possibilistic perfect operators maks information-flow event 2001 by michaelbanks on 2008-10-29 17:50:22 as read

	A unifying approach to the security of distributed and multi-threaded programs [My Copy] Journal of Computer Security, Vol. 11, No. 4. (1 January 2003), pp. 615-676. by Heiko Mantel, Andrei Sabelfeld posted to translation security program maks language information-flow distributed 2003 by michaelbanks on 2009-10-30 14:16:44 as
	Exploiting Generic Aspects of Security Models in Formal Developments [My Copy] Mechanizing Mathematical Reasoning In Mechanizing Mathematical Reasoning, Vol. 2605 (2005), pp. 452-475. by Heiko Mantel, Axel Schairer posted to security maks information-flow formal-methods 2005 by michaelbanks on 2009-10-19 19:18:02 as
	Automating proofs of unwinding conditions [My Copy] In Proceedings of the Verify'06 Verification Workshop (2006) by Dieter Hutter edited by Serge Autexier, Heiko Mantel posted to verification unwinding theorem-proving proof multi-agent maks information-flow automatic 2006 by michaelbanks on 2009-08-26 13:06:14 as
	Security of multi-agent systems: A case study on comparison shopping [My Copy] Journal of Applied Logic, Vol. 5, No. 2. (June 2007), pp. 303-332. by Dieter Hutter, Heiko Mantel, Ina Schaefer, Axel Schairer posted to security multi-agent case-study 2007 by michaelbanks on 2009-08-26 12:21:12 as
	Combining Different Proof Techniques for Verifying Information Flow Security [My Copy] Logic-Based Program Synthesis and Transformation In Logic-Based Program Synthesis and Transformation, Vol. 4407 (2007), pp. 94-110. by Heiko Mantel, Henning Sudbrock, Tina Kraußer posted to 2006 composition information-flow program proof security verification by michaelbanks on 2009-07-09 13:00:49 as
	The framework of selective interleaving functions and the modular assembly kit [My Copy] In FMSE '05: Proceedings of the 2005 ACM workshop on Formal methods in security engineering (2005), pp. 53-62. by Heiko Mantel posted to 2005 comparison information-flow maks property security selective-interleaving by michaelbanks on 2009-07-09 12:21:56 as
	On the Composition of Secure Systems [My Copy] Proceedings of the 2002 IEEE Symposium on Security and Privacy In Proceedings of the 2002 IEEE Symposium on Security and Privacy (2002), pp. 88-101. by Heiko Mantel posted to 2002 composition property security system by michaelbanks on 2008-11-25 16:06:36 as along with 1 person jfischer
	Possibilistic Definitions of Security --- an Assembly Kit [My Copy] 13th IEEE Computer Security Foundations Workshop (CSFW '00) In 13th IEEE Computer Security Foundations Workshop (CSFW '00) (2000), pp. 185-199. by Heiko Mantel posted to separability security possibilistic noninterference maks information-flow framework 2000 by michaelbanks on 2008-11-19 10:14:41 as
	Unwinding Possibilistic Security Properties [My Copy] Computer Security - ESORICS 2000 In Computer Security -- ESORICS 2000, Vol. 1895 (2000), pp. 238-254. by Heiko Mantel posted to 2000 nondeterministic noninterference possibilistic property refinement security theorem unwinding generalised by michaelbanks on 2008-11-01 18:46:39 as
	A Uniform Framework for the Formal Specification and Verification of Information Flow Security [My Copy] (July 2003) by Heiko Mantel posted to verification specification security maks information-flow framework formal 2003 by michaelbanks on 2008-10-29 17:50:22 as
	Preserving Information Flow Properties under Refinement [My Copy] In Proceedings of the 2001 IEEE Symposium on Security and Privacy (2001), pp. 78-91. by Heiko Mantel posted to specification security refinement property preserving possibilistic perfect operators maks information-flow event 2001 by michaelbanks on 2008-10-29 17:50:22 as

michaelbanks's Mantel:H [11 articles] Export

michaelbanks's tags

security	350
protocol	146
book	99
refinement	95
information-flow	90
specification	88
formal-methods	86
verification	79
2008	75
model	65
2006	64
proof	59
2009	59
property	58
attack	58
analysis	51
csp	51
2007	49
noninterference	49
formal	48
2005	48
logic	45
language	45
system	43
survey	42
2003	41
semantics	39
1996	38
z	37
software	35
textbook	35
confidentiality	35
programming	34
process-algebra	33
type-flaw	33
composition	32
program	31
2001	31
framework	30
policy	30
model-checking	29
theory	29
1995	29
tool	28
2000	27
authentication	27
introduction	27
software-engineering	26
automatic	26
1990	26
2002	26
1994	25
mathematics	25
2004	24
cryptography	24
1999	23
1997	23
1992	23
1998	22
concurrency	21
probabilistic	19
trace	19
1987	18
development	18
safety	18
bell-lapadula	18
access-control	18
theorem-proving	17
circus	16
distributed	16
1993	16
unwinding	16
commercial	16
needham-schroeder	15
possibilistic	15
algebraic	15
refinement-calculus	14
criticism	14
design	14
utp	14
testing	13
key	13
information	13
liveness	13
integrity	13
search	12
1989	12
1988	12
data	12
hacking	12
alloy	12
fdr	11
multi-level	11
maks	11
java	11
engineering	11
requirements	11
ban	11
preserving	11
bisimulation	11
nondeterministic	11
event-b	10
1991	10
correctness	10
case-study	10
haskell	10
synthesis	10
ccs	10
yahalom	10
nondeducibility	9
public	9
hoare-logic	9
availability	9
strand-space	9
1981	9
anonymity	9
type-system	9
reasoning	9
channels	9
operational	8
temporal	8
comparison	8
constraint-solving	8
privacy	8
simulation	8
dolev-yao	8
heuristic	8
b-method	8
verified-software-repository	8
knowledge	8
spi-calculus	8
belief	8
1985	8
category-theory	8
opinion	8
covert	7
1977	7
compiler	7
functional-programming	7
static-analysis	7
1986	7
kernel	7
guidance	7
neuman-stubblebine	7
1984	7
1978	7
automata	7
separability	7
tagging	7
rodin	6
executable	6
transformation	6
history	6
object-z	6
action	6
roundtable	6
communication	6
type-checking	6
denotational	6
replay	6
operating-system	6
tutorial	6
file-system	5
management	5
isabelle	5
precondition	5
coq	5
1976	5
mondex	5
structure	5
key-establishment	5
transitive	5
jif	5
svo	5
abstraction	5
derivation	5
multi-agent	5
predicate-transformer	5
role-based-access-control	5
paradox	5
philosophy	5
uml	5
standard	5
1983	5
optimisation	5
expressiveness	5
lattice	5
control-flow	5
generalised	5
decidability	5
pi-calculus	5
stepwise	5
grand-challenge	5
otway-rees	5
noninference	5
equivalence	4
vdm	4
axiomatic	4
casper	4
1980	4
z-eves	4
induction	4
tla	4
time	4
confinement	4
stairs	4
hol	4
resource-allocation	4
validation	4
implementation	4
1972	4
spa	4
posix	4
economics	4
state-machine	4
weakest	4
labelled-transition-system	4
review	4
guarded	4
game-theory	4
general	4
distribution	4
quantitative	4
1982	4
network	4
definition	4
deterministic	4
object-oriented	4
web-services	4
reliability	4
gdoi	4
selective-interleaving	4
biba	4
architecture	4
cipher-block-chaining	4
failures	4
model-driven	4
social-processes	3
methods	3
rewrite	3
advocacy	3
athena	3
internet	3
divergences	3
command	3
artificial-intelligence	3
flaw	3
computer	3
ponder	3
mechanised	3
trust	3
accountability	3
principles	3
declassification	3
lysa	3
simulated-annealing	3
usability	3
godel	3
capacity	3
1979	3
reconfigurable	3
denial-of-service	3
unifying	3
linking	3
window	3
abstract-interpretation	3
risk	3
chinese-wall	3
galois-connection	3
flow	3
predicate	3
genetic-algorithm	3
relational	3
recursion	3
predicate-calculus	3
inference-control	3
decomposition	3
no-silver-bullet	3
larch	3
1975	3
chaos-report	3
kerberos	3
password	3
voting	3
certification	3
event	3
1969	3
perfect	3
ada	3
raise	3
set-theory	3
non-functional	2
separation-of-duty	2
pattern-matching	2
virus	2
spore-library	2
diagram	2
focus	2
statistics	2
avispa	2
hypervisor	2
csp-oz	2
scyther	2
indistinguishable	2
closure	2
xen-hypervisor	2
safety-critical	2
research	2
guessing	2
contract	2
algorithm	2
teaching	2
project	2
andrew-secure-rpc	2
1973	2
incident-insensitive	2
mandatory-access-control	2
state-based	2
floating-point	2
translation	2
storage	2
nonce	2
dictionary	2
discretionary-access-control	2
1971	2
spi2java	2
ignorance	2
limitations	2
sequential	2
shadow-semantics	2
2010	2
retrieve-relation	2
clark-wilson	2
parser	2
hardware	2
complexity	2
topology	2
indistinguishability-classes	2
functionality	2
practical	2
genetic-programming	2
swift	2
xenon	2
natural	2
separation	2
tokeneer	2
efficient	2
s3a	2
restrictiveness	2
evaluation	2
algorithms	2
system-z	2
representation	2
multics	2
prolog	2
emergence	2
database	2
obligation	2
memory	2
finalisation	2
hyperproperty	2
reference	2
ckt5	2
sat-solver	2
assurance	2
theorem	2
fm	2
woo-lam	2
adaptation	2
dining-cryptographers	2
guidelines	2
kao-chow	2
dynamic	2
quantification	2
mix	2
operators	2
writing	2
extraction	2
possible-worlds	2
eiffel	2
capsl	2
pointers	2
timestamp	2
real-time	2
ibm-cics	2
1974	2
lambda-calculus	2
turing-award	2
separation-logic	2
mobile	2
computability	2
spark	2
hru	2
authenticity	2
relation	2
animation	2
records	2
refusals	1
visual	1
1970	1
backtracking	1
lasco	1
linear	1
linux	1
freshness	1
epistemic	1
information-theory	1
secpal	1
algebra	1
cscw	1
scam	1
probe	1
deadlock	1
psychology	1
modal	1
email	1
microsoft	1
cellphone	1
forward-correctability	1
self-reference	1
forwards	1
modularity	1
chosen-name	1
extreme-programming	1
b-toolkit	1
backwards	1
exception-handling	1
1962	1
fixed-point	1
curry-howard	1
quality	1
bndc	1
synchronisation	1
denning-sacco	1
non-repudiation	1
manifesto	1
aggregation	1
rsa	1
gny	1
crefine	1
graph-theory	1
iso-iec-11770-2	1
wide-mouthed-frog	1
behaviours	1
kripke-structure	1
intrusion-detection	1
rootkit	1
lightweight	1
numbers	1
conformance	1
smart-card	1
sharing	1
segregation	1
talk	1
signing	1
hazop	1
zero-knowledge	1
intel	1
xor	1
lecture	1
similarity	1
parsing-ambiguity	1
transputer	1
deterrent	1
computer-science	1
eclipse	1
incompleteness	1
execution	1
lazy	1
variables	1
isomorphism	1
punishment	1
jcsp	1
wireless-sensor	1
digital-restrictions	1
crime	1
term	1
aegis	1
declarative	1
monads	1
secure-electronic-transaction	1
1948	1
bpp	1
conflict-of-interest	1
domain	1
lecture-notes	1
petri-nets	1
virtual	1
ordering	1
1967	1
publishing	1
monitor	1
decoding	1
cut-and-paste	1
perfect-security-property	1
weak	1
may	1
eigen	1
nonfunctional	1
separation-of-concerns	1