-
Security Science (SecSci), Basic Concepts and Mathematical Foundations
Authors:
Dusko Pavlovic,
Peter-Michael Seidel
Abstract:
This textbook compiles the lecture notes from security courses taught at Oxford in the 2000s, at Royal Holloway in the 2010s, and currently in Hawaii. The early chapters are suitable for a first course in security. The middle chapters have been used in advanced courses. Towards the end there are also some research problems.
This textbook compiles the lecture notes from security courses taught at Oxford in the 2000s, at Royal Holloway in the 2010s, and currently in Hawaii. The early chapters are suitable for a first course in security. The middle chapters have been used in advanced courses. Towards the end there are also some research problems.
△ Less
Submitted 23 April, 2025;
originally announced April 2025.
-
How creative versus technical constraints affect individual learning in an online innovation community
Authors:
Victor P. Seidel,
Christoph Riedl
Abstract:
Online innovation communities allow for a search for novel solutions within a design space bounded by constraints. Past research has focused on the effect of creative constraints on individual projects, but less is known about how constraints affect learning from repeated design submissions and the effect of the technical constraints that are integral to online platforms. How do creative versus te…
▽ More
Online innovation communities allow for a search for novel solutions within a design space bounded by constraints. Past research has focused on the effect of creative constraints on individual projects, but less is known about how constraints affect learning from repeated design submissions and the effect of the technical constraints that are integral to online platforms. How do creative versus technical constraints affect individual learning in exploring a design space in online communities? We analyzed ten years of data from an online innovation community that crowdsourced 136,989 design submissions from 33,813 individuals. We leveraged data from two types of design contests-creatively constrained and unconstrained-running in parallel on the platform, and we evaluated a natural experiment where a platform change reduced technical constraints. We find that creative constraints lead to high rates of learning only if technical constraints are sufficiently relaxed. Our findings have implications for the management of creative design work and the downstream effects of the technical constraints of the information systems that support online innovation communities.
△ Less
Submitted 27 March, 2023;
originally announced March 2023.
-
Privacy protocols
Authors:
Jason Castiglione,
Dusko Pavlovic,
Peter-Michael Seidel
Abstract:
Security protocols enable secure communication over insecure channels. Privacy protocols enable private interactions over secure channels. Security protocols set up secure channels using cryptographic primitives. Privacy protocols set up private channels using secure channels. But just like some security protocols can be broken without breaking the underlying cryptography, some privacy protocols c…
▽ More
Security protocols enable secure communication over insecure channels. Privacy protocols enable private interactions over secure channels. Security protocols set up secure channels using cryptographic primitives. Privacy protocols set up private channels using secure channels. But just like some security protocols can be broken without breaking the underlying cryptography, some privacy protocols can be broken without breaking the underlying security. Such privacy attacks have been used to leverage e-commerce against targeted advertising from the outset; but their depth and scope became apparent only with the overwhelming advent of influence campaigns in politics. The blurred boundaries between privacy protocols and privacy attacks present a new challenge for protocol analysis. Covert channels turn out to be concealed not only below overt channels, but also above: subversions, and the level-below attacks are supplemented by sublimations and the level-above attacks.
△ Less
Submitted 11 April, 2019;
originally announced April 2019.
-
Quotients in monadic programming: Projective algebras are equivalent to coalgebras
Authors:
Dusko Pavlovic,
Peter-Michael Seidel
Abstract:
In monadic programming, datatypes are presented as free algebras, generated by data values, and by the algebraic operations and equations capturing some computational effects. These algebras are free in the sense that they satisfy just the equations imposed by their algebraic theory, and remain free of any additional equations. The consequence is that they do not admit quotient types. This is, of…
▽ More
In monadic programming, datatypes are presented as free algebras, generated by data values, and by the algebraic operations and equations capturing some computational effects. These algebras are free in the sense that they satisfy just the equations imposed by their algebraic theory, and remain free of any additional equations. The consequence is that they do not admit quotient types. This is, of course, often inconvenient. Whenever a computation involves data with multiple representatives, and they need to be identified according to some equations that are not satisfied by all data, the monadic programmer has to leave the universe of free algebras, and resort to explicit destructors. We characterize the situation when these destructors are preserved under all operations, and the resulting quotients of free algebras are also their subalgebras. Such quotients are called *projective*. Although popular in universal algebra, projective algebras did not attract much attention in the monadic setting, where they turn out to have a surprising avatar: for any given monad, a suitable category of projective algebras is equivalent with the category of coalgebras for the comonad induced by any monad resolution. For a monadic programmer, this equivalence provides a convenient way to implement polymorphic quotients as coalgebras. The dual correspondence of injective coalgebras and all algebras leads to a different family of quotient types, which seems to have a different family of applications. Both equivalences also entail several general corollaries concerning monadicity and comonadicity.
△ Less
Submitted 13 April, 2017; v1 submitted 26 January, 2017;
originally announced January 2017.
-
(Modular) Effect Algebras are Equivalent to (Frobenius) Antispecial Algebras
Authors:
Dusko Pavlovic,
Peter-Michael Seidel
Abstract:
Effect algebras are one of the generalizations of Boolean algebras proposed in the quest for a quantum logic. Frobenius algebras are a tool of categorical quantum mechanics, used to present various families of observables in abstract, often nonstandard frameworks. Both effect algebras and Frobenius algebras capture their respective fragments of quantum mechanics by elegant and succinct axioms; and…
▽ More
Effect algebras are one of the generalizations of Boolean algebras proposed in the quest for a quantum logic. Frobenius algebras are a tool of categorical quantum mechanics, used to present various families of observables in abstract, often nonstandard frameworks. Both effect algebras and Frobenius algebras capture their respective fragments of quantum mechanics by elegant and succinct axioms; and both come with their conceptual mysteries. A particularly elegant and mysterious constraint, imposed on Frobenius algebras to characterize a class of tripartite entangled states, is the antispecial law. A particularly contentious issue on the quantum logic side is the modularity law, proposed by von Neumann to mitigate the failure of distributivity of quantum logical connectives. We show that, if quantum logic and categorical quantum mechanics are formalized in the same framework, then the antispecial law of categorical quantum mechanics corresponds to the natural requirement of effect algebras that the units are each other's unique complements; and that the modularity law corresponds to the Frobenius condition. These correspondences lead to the equivalence announced in the title. Aligning the two formalisms, at the very least, sheds new light on the concepts that are more clearly displayed on one side than on the other (such as e.g. the orthogonality). Beyond that, it may also open up new approaches to deep and important problems of quantum mechanics (such as the classification of complementary observables).
△ Less
Submitted 3 January, 2017; v1 submitted 21 May, 2016;
originally announced May 2016.
-
Testing Randomness by Matching Pennies
Authors:
Dusko Pavlovic,
Peter-Michael Seidel,
Muzamil Yahia
Abstract:
In the game of Matching Pennies, Alice and Bob each hold a penny, and at every tick of the clock they simultaneously display the head or the tail sides of their coins. If they both display the same side, then Alice wins Bob's penny; if they display different sides, then Bob wins Alice's penny. To avoid giving the opponent a chance to win, both players seem to have nothing else to do but to randoml…
▽ More
In the game of Matching Pennies, Alice and Bob each hold a penny, and at every tick of the clock they simultaneously display the head or the tail sides of their coins. If they both display the same side, then Alice wins Bob's penny; if they display different sides, then Bob wins Alice's penny. To avoid giving the opponent a chance to win, both players seem to have nothing else to do but to randomly play heads and tails with equal frequencies. However, while not losing in this game is easy, not missing an opportunity to win is not. Randomizing your own moves can be made easy. Recognizing when the opponent's moves are not random can be arbitrarily hard.
The notion of randomness is central in game theory, but it is usually taken for granted. The notion of outsmarting is not central in game theory, but it is central in the practice of gaming. We pursue the idea that these two notions can be usefully viewed as two sides of the same coin.
△ Less
Submitted 2 February, 2018; v1 submitted 11 March, 2015;
originally announced March 2015.
-
Combinatorial Gradient Fields for 2D Images with Empirically Convergent Separatrices
Authors:
Jan Reininghaus,
David Günther,
Ingrid Hotz,
Tino Weinkauf,
Hans Peter Seidel
Abstract:
This paper proposes an efficient probabilistic method that computes combinatorial gradient fields for two dimensional image data. In contrast to existing algorithms, this approach yields a geometric Morse-Smale complex that converges almost surely to its continuous counterpart when the image resolution is increased. This approach is motivated using basic ideas from probability theory and builds up…
▽ More
This paper proposes an efficient probabilistic method that computes combinatorial gradient fields for two dimensional image data. In contrast to existing algorithms, this approach yields a geometric Morse-Smale complex that converges almost surely to its continuous counterpart when the image resolution is increased. This approach is motivated using basic ideas from probability theory and builds upon an algorithm from discrete Morse theory with a strong mathematical foundation. While a formal proof is only hinted at, we do provide a thorough numerical evaluation of our method and compare it to established algorithms.
△ Less
Submitted 31 August, 2012;
originally announced August 2012.
-
Formal Verification of an Iterative Low-Power x86 Floating-Point Multiplier with Redundant Feedback
Authors:
Peter-Michael Seidel
Abstract:
We present the formal verification of a low-power x86 floating-point multiplier. The multiplier operates iteratively and feeds back intermediate results in redundant representation. It supports x87 and SSE instructions in various precisions and can block the issuing of new instructions. The design has been optimized for low-power operation and has not been constrained by the formal verification…
▽ More
We present the formal verification of a low-power x86 floating-point multiplier. The multiplier operates iteratively and feeds back intermediate results in redundant representation. It supports x87 and SSE instructions in various precisions and can block the issuing of new instructions. The design has been optimized for low-power operation and has not been constrained by the formal verification effort. Additional improvements for the implementation were identified through formal verification. The formal verification of the design also incorporates the implementation of clock-gating and control logic. The core of the verification effort was based on ACL2 theorem proving. Additionally, model checking has been used to verify some properties of the floating-point scheduler that are relevant for the correct operation of the unit.
△ Less
Submitted 20 October, 2011;
originally announced October 2011.
