
@PREAMBLE{ {\providecommand{\ac}[1]{\textsc{#1}} } 
	 # {\providecommand{\acs}[1]{\textsc{#1}} } 
	 # {\providecommand{\acf}[1]{\textsc{#1}} } 
	 # {\providecommand{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } 
	 # {\providecommand{\leanTAP}{\mbox{\sf lean\it\TAP}} } 
	 # {\providecommand{\holz}{\textsc{hol-z}} } 
	 # {\providecommand{\holocl}{\textsc{hol-ocl}} } 
	 # {\providecommand{\isbn}{\textsc{isbn}} } 
         # {\providecommand{\Cpp}{C++} } 
         # {\providecommand{\Specsharp}{Spec\#} } 
	 # {\providecommand{\doi}[1]{\href{https://doi.org/#1}{doi:
	   {\urlstyle{rm}\nolinkurl{#1}}}}} }
@STRING{conf-tphols="\acs{tphols}" }
@STRING{iso	= {International Organization for Standardization} }
@STRING{j-ar	= "Journal of Automated Reasoning" }
@STRING{j-cacm	= "Communications of the \acs{acm}" }
@STRING{j-acta-informatica =  "Acta Informatica" }
@STRING{j-sosym	= "Software and Systems Modeling" }
@STRING{j-sttt	= "International Journal on Software Tools for Technology" }
@STRING{j-ist	= "Information and Software Technology" }
@STRING{j-toplas= "\acs{acm} Transactions on Programming Languages and
		  Systems" }
@STRING{j-tosem	= "\acs{acm} Transactions on Software Engineering and
		  Methodology" }
@STRING{j-eceasst="Electronic Communications of the \acs{easst}" }
@STRING{j-fac	= "Formal Aspects of Computing" }
@STRING{j-ucs	= "Journal of Universal Computer Science" }
@STRING{j-sl	= "Journal of Symbolic Logic" }
@STRING{j-fp	= "Journal of Functional Programming" }
@STRING{j-tkde	= {\acs{ieee} Transaction on Knowledge and Data Engineering} }
@STRING{j-tse	= {\acs{ieee} Transaction on Software Engineering} }
@STRING{j-entcs	= {Electronic Notes in Theoretical Computer Science} }
@STRING{s-lnai  = "Lecture Notes in Computer Science" }
@STRING{s-lncs  = "Lecture Notes in Computer Science" }
@STRING{s-lnbip = "Lecture Notes in Business Information Processing" }
@String{j-computer = "Computer"}
@String{j-tissec = "\acs{acm} Transactions on Information and System Security"}
@STRING{omg	= {Object Management Group} }
@STRING{j-ipl   = {Information Processing Letters} }
@STRING{j-login	= ";login: the USENIX Association newsletter" }

@STRING{PROC = "Proceedings of the " }


% Publisher:
% ==========
@STRING{pub-awl	= {Addison-Wesley Longman, Inc.} }
@STRING{pub-awl:adr={Reading, MA, \acs{usa}} }
@STRING{pub-springer={Springer-Verlag} }
@STRING{pub-springer:adr={Heidelberg} }
@STRING{pub-cup	= {Cambridge University Press} }
@STRING{pub-cup:adr={New York, \acs{ny}, \acs{usa}} }
@STRING{pub-mit	= {\acs{mit} Press} }
@STRING{pub-mit:adr={Cambridge, Massachusetts} }
@STRING{pub-springer-ny={Springer-Verlag} }
,
@STRING{pub-springer-netherlands={Springer Netherlands} }
@STRING{pub-springer-netherlands:adr={} }
@STRING{pub-springer-ny:adr={New York, \acs{ny}, \acs{usa}} }
@STRING{pub-springer-london={Springer-Verlag} }
@STRING{pub-springer-london:adr={London} }
@STRING{pub-ieee= {\acs{ieee} Computer Society} }
@STRING{pub-ieee:adr={Los Alamitos, \acs{ca}, \acs{usa}} }
@STRING{pub-prentice={Prentice Hall, Inc.} }
@STRING{pub-prentice:adr={Upper Saddle River, \acs{nj}, \acs{usa}} }
@STRING{pub-acm	= {\acs{acm} Press} }
@STRING{pub-acm:adr={New York, \acs{ny} \acs{usa}} }
@STRING{pub-oxford={Oxford University Press, Inc.} }
@STRING{pub-oxford:adr={New York, \acs{ny}, \acs{usa}} }
@STRING{pub-kluwer={Kluwer Academic Publishers} }
@STRING{pub-kluwer:adr={Dordrecht} }
@STRING{pub-elsevier={Elsevier Science Publishers} }
@STRING{pub-elsevier:adr={Amsterdam} }
@STRING{pub-north={North-Holland Publishing Co.} }
@STRING{pub-north:adr={Nijmegen, The Netherlands} }
@STRING{pub-ios	= {\textsc{ios} Press} }
@STRING{pub-ios:adr={Amsterdam, The Netherlands} }
@STRING{pub-heise={Heise Zeitschriften Verlag} }
@STRING{pub-heise:adr={Hannover, Germany} }


@INPROCEEDINGS{brucker.ea:icst:2010,
  author = {Achim D. Brucker and Lukas Br\"ugger and Paul Kearney and Burkhart Wolff},
  title = {Verified Firewall Policy Transformations for Test Case Generation},
  year = 2010,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  copyright = {\copyright Springer-Verlag},
  booktitle = {International Conference on Software Testing {(ICST10)}},
  location = {Paris, France},
  editor = {Ana Cavalli and Sudipto Ghosh},
  annote = {To appear in LNCS},
  classification = {conference},
  pdf = {../papers/conf/firewall-reloaded.pdf},
  abstract = {We present an optimization technique for model-based generation of
  test cases for firewalls. Based on a formal model for firewall
  policies in higher-order logic, we derive a collection of
  semantics-preserving policy transformation rules and an algorithm
  that optimizes the specification with respect of the number of
  test cases required for path coverage.  The correctness of the rules
  and the algorithm is established by formal proofs in
  Isabelle/\acs{hol}. Finally, we use the normalized policies to
  generate test cases with the domain-specific firewall testing tool
  \testgenFW.
 
  The resulting procedure is characterized by a gain in efficiency
  of two orders of magnitude and can handle configurations with
  hundreds of rules as occur in practice.
 
  Our approach can be seen as an instance of a methodology to
  tame inherent state-space explosions in test case generation for
  security policies.}
}


@InCollection{	  brucker.ea:test-sequence:2007,
  abstract	= {HOL-TestGen is a specification and test-case generation
		  environment extending the interactive theorem prover
		  Isabelle/HOL. Its method is two-staged: first, the
		  original formula is partitioned into test cases by
		  transformation into a normal form. Second, the test cases
		  are analyzed for ground instances (the test data)
		  satisfying the constraints of the test cases. Particular
		  emphasis is put on the control of explicit test hypotheses
		  which can be proven over concrete programs.
		  
		  Although originally designed for black-box unit-tests,
		  HOL-TestGen's underlying logic and deduction engine is
		  powerful enough to be used in test-sequence generation, too.
		  
		  We develop the theory for test-sequence generation with
		  HOL-TestGen and describe its use in a substantial case-study
		  in the field of computer security, namely the black-box
		  test of configured firewalls. },
  keywords	= {security, model-based testing, specification-based
		  testing, firewall testing},
  location	= {Zurich},
  author	= {Achim D. Brucker and Burkhart Wolff},
  booktitle	= {TAP 2007: Tests And Proofs},
  language	= {USenglish},
  publisher	= pub-springer,
  series	= s-lncs,
  number	= 4454,
  editor	= {Bertrand Meyer and Yuri Gurevich},
  title		= {Test-Sequence Generation with {HOL-TestGen} -- With an
		  Application to Firewall Testing },
  categories	= {holtestgen},
  classification= {conference},
  public	= {yes},
  year		= 2007,
  doi		= {10.1007/978-3-540-73770-4_9},
  pages		= {149--168},
  pdf		= {http://www.brucker.ch/bibliography/download/2007/brucker.ea-test-sequence-2007.pdf}
		  ,
  ps		= {http://www.brucker.ch/bibliography/download/2007/brucker.ea-test-sequence-2007.ps.gz}
		  ,
		  
}

@InCollection{	  brucker.ea:model-based:2008,
  abstract	= {Firewalls are a cornerstone of todays security
		  infrastructure for networks. Their configuration,
		  implementing a firewall policy, is inherently complex, hard
		  to understand, and difficult to validate.
		  
		  We present a substantial case study performed with the
		  model-based testing tool HOL-TestGen. Based on a formal model
		  of firewalls and their policies in HOL, we first
		  present a derived theory for simplifying policies. We
		  discuss different test plans for test specifications.
		  Finally, we show how to integrate these issues to a
		  domain-specific firewall testing tool HOL-TestGen/FW.},
  editor	= {Kenji Suzuki and Teruo Higashino},
  location	= {Tokyo, Japan},
  author	= {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
  booktitle	= {Testcom/FATES 2008},
  language	= {USenglish},
  publisher	= pub-springer,
  series	= s-lncs,
  number	= 5047,
  doi		= {10.1007/978-3-540-68524-1_9},
  pages		= {103--118},
  title		= {Model-based Firewall Conformance Testing},
  categories	= {holtestgen},
  classification= {conference},
  year		= 2008,
  pdf		= {http://www.brucker.ch/bibliography/download/2008/brucker.ea-model-based-2008.pdf}
		  ,
  ps		= {http://www.brucker.ch/bibliography/download/2008/brucker.ea-model-based-2008.ps.gz}
		  ,
  public	= {yes},
		  
}

@PhDThesis{       bidder:specification:2007,
  author        = {Diana von Bidder},
  title         = {Specification-based Firewall Testing},
  school        = {ETH Zurich},
  year          = 2007,
  public        = {yes},
  type          = {Ph.D. Thesis},
  acknowledgement={none},
  classification= {thesis},
  note          = {\acs{eth} Dissertation No. 17172. Diana von Bidder's
                  maiden name is Diana Senn.}
}

 	

@article{Network_Security_Policy_Verification-AFP,
  author  = {Cornelius Diekmann},
  title   = {Network Security Policy Verification},
  journal = {Archive of Formal Proofs},
  month   = jul,
  year    = 2014,
  note    = {\url{http://isa-afp.org/entries/Network_Security_Policy_Verification.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}

@Article{ brucker.ea:upf:2014,
	abstract	= 	{We present the Unified Policy Framework (UPF), a generic framework for modelling security (access-control) policies. UPF emphasizes the view that a policy is a policy decision function that grants or denies access to resources, permissions, etc. In other words, instead of modelling the relations of permitted or prohibited requests directly, we model the concrete function that implements the policy decision point in a system. In more detail, UPF is based on the following four principles: 1) Functional representation of policies, 2) No conflicts are possible, 3) Three-valued decision type (allow, deny, undefined), 4) Output type not containing the decision only.},
	author	= 	{Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
	date	= 	{2014-11-28},
	file	= 	{https://www.brucker.ch/bibliography/download/2014/brucker.ea-upf-outline-2014.pdf},
	filelabel	= 	{Outline},
	issn	= 	{2150-914x},
	journal	= 	{Archive of Formal Proofs},
	month	= 	{sep},
	note	= 	{\url{http://www.isa-afp.org/entries/UPF.shtml}, Formal proof development},
	pdf	= 	{https://www.brucker.ch/bibliography/download/2014/brucker.ea-upf-2014.pdf},
	title	= 	{The Unified Policy Framework (UPF)},
	url	= 	{https://www.brucker.ch/bibliography/abstract/brucker.ea-upf-2014},
	year	= 	{2014},
} 
@Article{ brucker.ea:formal-fw-testing:2014,
	abstract	= 	{Firewalls are an important means to secure critical ICT infrastructures. As configurable off-the-shelf prod\-ucts, the effectiveness of a firewall crucially depends on both the correctness of the implementation itself as well as the correct configuration. While testing the implementation can be done once by the manufacturer, the configuration needs to be tested for each application individually. This is particularly challenging as the configuration, implementing a firewall policy, is inherently complex, hard to understand, administrated by different stakeholders and thus difficult to validate. This paper presents a formal model of both stateless and stateful firewalls (packet filters), including NAT, to which a specification-based conformance test case gen\-eration approach is applied. Furthermore, a verified optimisation technique for this approach is presented: starting from a formal model for stateless firewalls, a collection of semantics-preserving policy transformation rules and an algorithm that optimizes the specification with respect of the number of test cases required for path coverage of the model are derived. We extend an existing approach that integrates verification and testing, that is, tests and proofs to support conformance testing of network policies. The presented approach is supported by a test framework that allows to test actual firewalls using the test cases generated on the basis of the formal model. Finally, a report on several larger case studies is presented.},
	author	= 	{Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
	doi	= 	{10.1002/stvr.1544},
	journal	= 	{Software Testing, Verification \& Reliability (STVR)},
	keywords	= 	{model-based testing; conformance testing; security testing; firewall; specification-based testing; testing cloud infrastructure, transformation for testability; HOL-TestGen; test and proof; security configuration testing},
	language	= 	{USenglish},
	number	= 	{1},
	pages	= 	{34--71},
	pdf	= 	{https://www.brucker.ch/bibliography/download/2014/brucker.ea-formal-fw-testing-2014.pdf},
	publisher	= 	{John Wiley \& Sons},
	title	= 	{Formal Firewall Conformance Testing: An Application of Test and Proof Techniques},
	url	= 	{https://www.brucker.ch/bibliography/abstract/brucker.ea-formal-fw-testing-2014},
	volume	= 	{25},
	year	= 	{2015},
} 

@Book{            spivey:z-notation:1992,
  bibkey        = {spivey:z-notation:1992},
  author        = {J. M. Spivey},
  title         = {The {Z} Notation: A Reference Manual},
  publisher     = pub-prentice,
  address       = pub-prentice:adr,
  edition       = {2nd},
  length        = 150,
  year          = 1992,
  isbn          = {0-139-78529-9},
  acknowledgement={brucker, 2007-04-23},
  abstract      = {This is a revised edition of the first widely available
                  reference manual on Z originally published in 1989. The
                  book provides a complete and definitive guide to the use of
                  Z in specifying information systems, writing specifications
                  and designing implementations. \par Contents: Tutorial
                  introduction; Background; The Z language; The mathematical
                  tool-kit; Sequential systems; Syntax summary; Changes from
                  the first edition; Glossary.}
}

@InCollection{    brucker.ea:hol-testgen-fw:2013,
  abstract      = { The \testgen environment is conceived as a system for
                  modeling and semi-automated test generation with an
                  emphasis on expressive power and generality. However, its
                  underlying technical framework Isabelle/\acs{hol} supports the
                  customization as well as the development of highly
                  automated add-ons working in specific application domains.

                  In this paper, we present \testgen/fw, an add-on for the
                  test framework \testgen, that allows for testing the
                  conformance of firewall implementations to high-level
                  security policies. Based on generic theories specifying a
                  security-policy language, we developed specific theories
                  for network data and firewall policies. On top of these
                  firewall specific theories, we provide mechanisms for
                  policy transformations based on derived rules and adapted
                  code-generators producing test drivers. Our empirical
                  evaluations shows that \testgen/fw is a competitive
                  environment for testing firewalls or high-level policies of
                  local networks. },
  keywords      = {symbolic test case generations, black box testing, theorem
                  proving, network security, firewall testing, conformance
                  testing},
  location      = {Shanghai},
  author        = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
  booktitle     = {International Colloquium on Theoretical Aspects of
                  Computing (\acs{ictac})},
  language      = {USenglish},
  publisher     = pub-springer,
  series        = s-lncs,
  number        = 8049,
  doi           = {10.1007/978-3-642-39718-9_7},
  editor        = {Zhiming Liu and Jim Woodcock and Huibiao Zhu},
  title         = {HOl-TestGen/FW: An Environment for Specification-based
                  Firewall Conformance Testing},
  categories    = {holtestgen},
  classification= {conference},
  areas         = {security, formal methods},
  public        = {yes},
  year          = 2013,
  pages         = {112--121},
  isbn          = {978-3-642-39717-2},
}
@Article{         brucker.ea:theorem-prover:2012,
  author        = {Achim D. Brucker and Burkhart Wolff},
  journal       = j-fac,
  publisher     = pub-springer,
  language      = {USenglish},
  categories    = {holtestgen},
  title         = {On Theorem Prover-based Testing},
  year          = 2013,
  issn          = {0934-5043},
  pages         = {683--721},
  volume        = 25,
  number        = 5,
  classification= {journal},
  areas         = {formal methods, software},
  public        = {yes},
  doi           = {10.1007/s00165-012-0222-y},
  keywords      = {test case generation, domain partitioning, test sequence,
                  theorem proving, \testgen},
  abstract      = {\testgen is a specification and test case generation
                  environment extending the interactive theorem prover
                  Isabelle/\acs{hol}. As such, \testgen allows for an integrated
                  workflow supporting interactive theorem proving, test case
                  generation, and test data generation.

                  The \testgen method is two-staged: first, the original
                  formula is partitioned into test cases by transformation
                  into a normal form called test theorem. Second, the test
                  cases are analyzed for ground instances (the test data)
                  satisfying the constraints of the test cases. Particular
                  emphasis is put on the control of explicit test-hypotheses
                  which can be proven over concrete programs.

                  Due to the generality of the underlying framework, our
                  system can be used for black-box unit, sequence, reactive
                  sequence and white-box test scenarios. Although based on
                  particularly clean theoretical foundations, the system can
                  be applied for substantial case-studies. },
}


@InProceedings{   brucker.ea:model-based:2011,
  title         = {An Approach to Modular and Testable Security Models of
                  Real-world Health-care Applications},
  author        = {Achim D. Brucker and Lukas Br{\"u}gger and Paul Kearney
                  and Burkhart Wolff},
  booktitle     = conf-sacmat,
  language      = {USenglish},
  publisher     = pub-acm,
  location      = {Innsbruck, Austria},
  categories    = {holtestgen},
  classification= {conference},
  areas         = {security, formal methods},
  year          = 2011,
  copyright     = {\acs{acm}},
  copyrighturl  = {http://dl.acm.org/authorize?431936},
  public        = {yes},
  pages         = {133--142},
  abstract      = {We present a generic modular policy modelling framework
                  and instantiate it with a substantial case study for
                  model-based testing of some key security mechanisms of
                  applications and services of the NPfIT. NPfIT, the National
                  Programme for \acs{it}, is a very large-scale development project
                  aiming to modernise the \acs{it} infrastructure of the \acs{nhs} in
                  England. Consisting of heterogeneous and distributed
                  applications, it is an ideal target for model-based testing
                  techniques of a large system exhibiting critical security
                  features.

                  We model the four information governance principles,
                  comprising a role-based access control model, as well as
                  policy rules governing the concepts of patient consent,
                  sealed envelopes and legitimate relationship. The model is
                  given in \acs{hol} and processed together with suitable test
                  specifications in the \testgen system, that generates
                  test sequences according to them. Particular emphasis is
                  put on the modular description of security policies and
                  their generic combination and its consequences for
                  model-based testing.},
  doi           = {10.1145/1998441.1998461},
  isbn          = {978-1-4503-0688-1},
}

@InCollection{    brucker.ea:interactive:2005,
  keywords      = {symbolic test case generations, black box testing, white
                  box testing, theorem proving, interactive testing},
  abstract      = {\testgen is a test environment for specification-based
                  unit testing build upon the proof assistant Isabelle/\acs{hol}\@.
                  While there is considerable skepticism with regard to
                  interactive theorem provers in testing communities, we
                  argue that they are a natural choice for (automated)
                  symbolic computations underlying systematic tests. This
                  holds in particular for the development on non-trivial
                  formal test plans of complex software, where some parts of
                  the overall activity require inherently guidance by a test
                  engineer. In this paper, we present the underlying methods
                  for both black box and white box testing in interactive
                  unit test scenarios. \testgen can also be understood as
                  a unifying technical and conceptual framework for
                  presenting and investigating the variety of unit test
                  techniques in a logically consistent way. },
  location      = {Edinburgh},
  author        = {Achim D. Brucker and Burkhart Wolff},
  booktitle     = {Formal Approaches to Testing of Software},
  language      = {USenglish},
  publisher     = pub-springer,
  series        = s-lncs,
  number        = 3997,
  doi           = {10.1007/11759744_7},
  isbn          = {3-540-25109-X},
  editor        = {Wolfgang Grieskamp and Carsten Weise},
  project       = {\acs{csfmdos}},
  title         = {Interactive Testing using \testgen},
  classification= {workshop},
  areas         = {formal methods, software},
  categories    = {holtestgen},
  year          = 2005,
  public        = {yes},
}

